Bob is cold. Bob is round. Bob is smart. Charlie is cold. Dave is blue. Dave is quiet. Harry is big. If someone is big then they are blue. All round people are cold. Rough people are cold. Blue people are round. If Harry is round and Harry is rough then Harry is cold. Round people are big.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Harry is big.
("Harry" "is" "big" "+")
If someone is big then they are blue.
((("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
All round people are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
Rough people are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
Blue people are round.
((("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If Harry is round and Harry is rough then Harry is cold.
((("Harry" "is" "round" "+") ("Harry" "is" "rough" "+")) -> ("Harry" "is" "cold" "+"))
Round people are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
Bob is cold.
True
1
proof
[(triple1 OR ((triple2) -> rule2))]
("Bob" "is" "cold" "+")
triple1
((triple2) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is not round.
False
1
inv-proof
[(triple2)]
("Bob" "is" "round" "-")
triple2
Bob is big.
True
2
proof
[(((triple2) -> rule6))]
("Bob" "is" "big" "+")
((triple2) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Dave is not round.
False
2
inv-proof
[(((triple5) -> rule4))]
("Dave" "is" "round" "-")
((triple5) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Harry is round.
True
3
proof
[(((((triple7) -> rule1)) -> rule4))]
("Harry" "is" "round" "+")
((((triple7) -> (rule1 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Dave is not big.
False
3
inv-proof
[(((((triple5) -> rule4)) -> rule6))]
("Dave" "is" "big" "-")
((((triple5) -> (rule4 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Harry is cold.
True
4
proof
[(((((((triple7) -> rule1)) -> rule4)) -> rule2))]
("Harry" "is" "cold" "+")
((((((triple7) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is not cold.
False
4
inv-proof
[(((((((triple7) -> rule1)) -> rule4)) -> rule2))]
("Harry" "is" "cold" "-")
((((((triple7) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Charlie is not big.
Unknown
inv-rconc
[@3: Charlie is big.[CWA. Example of deepest failure = (rule6 <- rule4 <- rule1 <- FAIL)]]
("Charlie" "is" "big" "-")
Charlie is blue.
Unknown
rconc
[@3: Charlie is blue.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule4 <- FAIL)]]
("Charlie" "is" "blue" "+")
Charlie is not round.
Unknown
inv-rconc
[@3: Charlie is round.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule6 <- FAIL)]]
("Charlie" "is" "round" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Bob is cold.[(triple1 OR ((triple2) -> rule2))] Bob is round.[(triple2)] Bob is smart.[(triple3)] Charlie is cold.[(triple4)] Dave is blue.[(triple5)] Dave is quiet.[(triple6)] Harry is big.[(triple7)] @1: Bob is big.[(((triple2) -> rule6))] Dave is round.[(((triple5) -> rule4))] Harry is blue.[(((triple7) -> rule1))] @2: Bob is blue.[(((((triple2) -> rule6)) -> rule1))] Dave is big.[(((((triple5) -> rule4)) -> rule6))] Dave is cold.[(((((triple5) -> rule4)) -> rule2))] Harry is round.[(((((triple7) -> rule1)) -> rule4))] @3: Harry is cold.[(((((((triple7) -> rule1)) -> rule4)) -> rule2))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
((triple2) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Charlie is cold.
("Charlie" "is" "cold" "+")
triple4
Dave is blue.
("Dave" "is" "blue" "+")
triple5
Dave is quiet.
("Dave" "is" "quiet" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
Bob is big.
("Bob" "is" "big" "+")
((triple2) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple5) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple7) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((((triple5) -> (rule4 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((((triple5) -> (rule4 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((((triple7) -> (rule1 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((((((triple7) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3