Anne is green. Bob is white. Fiona is green. If Bob is round then Bob is furry. If something is big then it is round. Round, blue things are red. All furry things are green. All round, big things are blue. All white things are round.
Anne is green.
("Anne" "is" "green" "+")
Bob is white.
("Bob" "is" "white" "+")
Fiona is green.
("Fiona" "is" "green" "+")
If Bob is round then Bob is furry.
((("Bob" "is" "round" "+")) -> ("Bob" "is" "furry" "+"))
If something is big then it is round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
Round, blue things are red.
((("something" "is" "round" "+") ("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
All furry things are green.
((("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
All round, big things are blue.
((("something" "is" "round" "+") ("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
All white things are round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
Anne is green.
True
1
proof
[(triple1)]
("Anne" "is" "green" "+")
triple1
Anne is not green.
False
1
inv-proof
[(triple1)]
("Anne" "is" "green" "-")
triple1
Bob is round.
True
2
proof
[(((triple2) -> rule6))]
("Bob" "is" "round" "+")
((triple2) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not round.
False
2
inv-proof
[(((triple2) -> rule6))]
("Bob" "is" "round" "-")
((triple2) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is furry.
True
3
proof
[(((((triple2) -> rule6)) -> rule1))]
("Bob" "is" "furry" "+")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is not furry.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule1))]
("Bob" "is" "furry" "-")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
True
4
proof
[(((((((triple2) -> rule6)) -> rule1)) -> rule4))]
("Bob" "is" "green" "+")
((((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is not green.
False
4
inv-proof
[(((((((triple2) -> rule6)) -> rule1)) -> rule4))]
("Bob" "is" "green" "-")
((((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Anne is not round.
Unknown
inv-rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "round" "-")
Anne is blue.
Unknown
rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "blue" "+")
Fiona is not red.
Unknown
inv-rconc
[@2: Fiona is red.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Fiona" "is" "red" "-")
Bob is red.
Unknown
rconc
[@2: Bob is red.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Bob" "is" "red" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
Fiona is not white.
Unknown
inv-random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
@0: Anne is green.[(triple1)] Bob is white.[(triple2)] Fiona is green.[(triple3)] @1: Bob is round.[(((triple2) -> rule6))] @2: Bob is furry.[(((((triple2) -> rule6)) -> rule1))] @3: Bob is green.[(((((((triple2) -> rule6)) -> rule1)) -> rule4))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Fiona is green.
("Fiona" "is" "green" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
((triple2) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3