Bob is cold. Bob is furry. Bob is rough. Bob is smart. Charlie is green. Dave is cold. Dave is furry. Dave is green. Dave is red. Dave is rough. Dave is smart. Dave is white. Fiona is furry. Fiona is green. Fiona is red. If someone is furry then they are cold. If someone is furry and smart then they are green. If Bob is red then Bob is green. Smart, green people are white. If someone is furry then they are cold. All rough, white people are red.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is red.
("Fiona" "is" "red" "+")
If someone is furry then they are cold.
((("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
If someone is furry and smart then they are green.
((("someone" "is" "furry" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
If Bob is red then Bob is green.
((("Bob" "is" "red" "+")) -> ("Bob" "is" "green" "+"))
Smart, green people are white.
((("someone" "is" "smart" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
If someone is furry then they are cold.
((("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
All rough, white people are red.
((("someone" "is" "rough" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
Bob is furry.
True
1
proof
[(triple2)]
("Bob" "is" "furry" "+")
triple2
Bob is not rough.
False
1
inv-proof
[(triple3)]
("Bob" "is" "rough" "-")
triple3
Fiona is cold.
True
2
proof
[(((triple13) -> rule1) OR ((triple13) -> rule5))]
("Fiona" "is" "cold" "+")
((triple13) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple13) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is not cold.
False
2
inv-proof
[(((triple13) -> rule1) OR ((triple13) -> rule5))]
("Fiona" "is" "cold" "-")
((triple13) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple13) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Bob is white.
True
5
proof
[(((triple4 ((triple2 triple4) -> rule2)) -> rule4))]
("Bob" "is" "white" "+")
((triple4 ((triple2 triple4) -> (rule2 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not white.
False
5
inv-proof
[(((triple4 ((triple2 triple4) -> rule2)) -> rule4))]
("Bob" "is" "white" "-")
((triple4 ((triple2 triple4) -> (rule2 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is red.
True
7
proof
[(((triple3 ((triple4 ((triple2 triple4) -> rule2)) -> rule4)) -> rule6))]
("Bob" "is" "red" "+")
((triple3 ((triple4 ((triple2 triple4) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is not red.
False
7
inv-proof
[(((triple3 ((triple4 ((triple2 triple4) -> rule2)) -> rule4)) -> rule6))]
("Bob" "is" "red" "-")
((triple3 ((triple4 ((triple2 triple4) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Fiona is not white.
Unknown
inv-rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "white" "-")
Charlie is white.
Unknown
rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "white" "+")
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is red.
Unknown
rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "red" "+")
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
Fiona is not rough.
Unknown
inv-random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Bob is cold.[(triple1 OR ((triple2) -> rule1) OR ((triple2) -> rule5))] Bob is furry.[(triple2)] Bob is rough.[(triple3)] Bob is smart.[(triple4)] Charlie is green.[(triple5)] Dave is cold.[(triple6 OR ((triple7) -> rule1) OR ((triple7) -> rule5))] Dave is furry.[(triple7)] Dave is green.[(triple8 OR ((triple7 triple11) -> rule2))] Dave is red.[(triple9 OR ((triple10 triple12) -> rule6) OR ((triple10 ((triple11 triple8) -> rule4)) -> rule6) OR ((triple10 ((triple11 ((triple7 triple11) -> rule2)) -> rule4)) -> rule6))] Dave is rough.[(triple10)] Dave is smart.[(triple11)] Dave is white.[(triple12 OR ((triple11 triple8) -> rule4) OR ((triple11 ((triple7 triple11) -> rule2)) -> rule4))] Fiona is furry.[(triple13)] Fiona is green.[(triple14)] Fiona is red.[(triple15)] @1: Bob is green.[(((triple2 triple4) -> rule2))] Fiona is cold.[(((triple13) -> rule1) OR ((triple13) -> rule5))] @2: Bob is white.[(((triple4 ((triple2 triple4) -> rule2)) -> rule4))] @3: Bob is red.[(((triple3 ((triple4 ((triple2 triple4) -> rule2)) -> rule4)) -> rule6))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
((triple2) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple2) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Charlie is green.
("Charlie" "is" "green" "+")
triple5
Dave is cold.
("Dave" "is" "cold" "+")
triple6
((triple7) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((triple7) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
triple7
Dave is green.
("Dave" "is" "green" "+")
triple8
((triple7 triple11) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple9
((triple10 triple12) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple10 ((triple11 triple8) -> (rule4 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((triple10 ((triple11 ((triple7 triple11) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
triple10
Dave is smart.
("Dave" "is" "smart" "+")
triple11
Dave is white.
("Dave" "is" "white" "+")
triple12
((triple11 triple8) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple11 ((triple7 triple11) -> (rule2 % int2))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple13
Fiona is green.
("Fiona" "is" "green" "+")
triple14
Fiona is red.
("Fiona" "is" "red" "+")
triple15
Bob is green.
("Bob" "is" "green" "+")
((triple2 triple4) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple13) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple13) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((triple4 ((triple2 triple4) -> (rule2 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((triple3 ((triple4 ((triple2 triple4) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3