Bob is big. Bob is cold. Bob is furry. Bob is nice. Bob is quiet. Bob is rough. Charlie is blue. Charlie is furry. Charlie is quiet. Dave is big. Dave is blue. Dave is furry. Dave is nice. Dave is quiet. Dave is rough. If something is big and cold then it is blue. If Bob is cold then Bob is rough. If Dave is cold then Dave is quiet. Blue, cold things are nice. All quiet, nice things are big. If something is rough and cold then it is blue. If Charlie is nice then Charlie is big. If something is big then it is rough.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
If something is big and cold then it is blue.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
If Bob is cold then Bob is rough.
((("Bob" "is" "cold" "+")) -> ("Bob" "is" "rough" "+"))
If Dave is cold then Dave is quiet.
((("Dave" "is" "cold" "+")) -> ("Dave" "is" "quiet" "+"))
Blue, cold things are nice.
((("something" "is" "blue" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
All quiet, nice things are big.
((("something" "is" "quiet" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If something is rough and cold then it is blue.
((("something" "is" "rough" "+") ("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
If Charlie is nice then Charlie is big.
((("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "big" "+"))
If something is big then it is rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
Dave is blue.
True
1
proof
[(triple11)]
("Dave" "is" "blue" "+")
triple11
Bob is not nice.
False
1
inv-proof
[(triple4 OR ((((triple1 triple2) -> rule1) triple2) -> rule4) OR ((((triple6 triple2) -> rule6) triple2) -> rule4) OR ((((((triple1) -> rule8) triple2) -> rule6) triple2) -> rule4) OR ((((((triple2) -> rule2) triple2) -> rule6) triple2) -> rule4))]
("Bob" "is" "nice" "-")
triple4
((((triple1 triple2) -> (rule1 % int2)) triple2) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple6 triple2) -> (rule6 % int2)) triple2) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((((triple1) -> (rule8 % int3)) triple2) -> (rule6 % int2)) triple2) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
((((((triple2) -> (rule2 % int3)) triple2) -> (rule6 % int2)) triple2) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is blue.
True
3
proof
[(((triple1 triple2) -> rule1) OR ((triple6 triple2) -> rule6) OR ((((triple1) -> rule8) triple2) -> rule6) OR ((((triple2) -> rule2) triple2) -> rule6) OR ((((triple5 triple4) -> rule5) triple2) -> rule1) OR ((((((triple5 triple4) -> rule5)) -> rule8) triple2) -> rule6))]
("Bob" "is" "blue" "+")
((triple1 triple2) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((triple6 triple2) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple1) -> (rule8 % int2)) triple2) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple2) -> (rule2 % int2)) triple2) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple5 triple4) -> (rule5 % int2)) triple2) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((((triple5 triple4) -> (rule5 % int3))) -> (rule8 % int2)) triple2) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is not blue.
False
3
inv-proof
[(((triple1 triple2) -> rule1) OR ((triple6 triple2) -> rule6) OR ((((triple1) -> rule8) triple2) -> rule6) OR ((((triple2) -> rule2) triple2) -> rule6) OR ((((triple5 triple4) -> rule5) triple2) -> rule1) OR ((((((triple5 triple4) -> rule5)) -> rule8) triple2) -> rule6))]
("Bob" "is" "blue" "-")
((triple1 triple2) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((triple6 triple2) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple1) -> (rule8 % int2)) triple2) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple2) -> (rule2 % int2)) triple2) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple5 triple4) -> (rule5 % int2)) triple2) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((((triple5 triple4) -> (rule5 % int3))) -> (rule8 % int2)) triple2) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Charlie is not rough.
Unknown
inv-rconc
[@3: Charlie is rough.[CWA. Example of deepest failure = (rule8 <- rule5 <- rule4 <- FAIL)]]
("Charlie" "is" "rough" "-")
Charlie is nice.
Unknown
rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "nice" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
@0: Bob is big.[(triple1 OR ((triple5 triple4) -> rule5) OR ((triple5 ((((triple6 triple2) -> rule6) triple2) -> rule4)) -> rule5) OR ((triple5 ((((((triple2) -> rule2) triple2) -> rule6) triple2) -> rule4)) -> rule5))] Bob is cold.[(triple2)] Bob is furry.[(triple3)] Bob is nice.[(triple4 OR ((((triple1 triple2) -> rule1) triple2) -> rule4) OR ((((triple6 triple2) -> rule6) triple2) -> rule4) OR ((((((triple1) -> rule8) triple2) -> rule6) triple2) -> rule4) OR ((((((triple2) -> rule2) triple2) -> rule6) triple2) -> rule4))] Bob is quiet.[(triple5)] Bob is rough.[(triple6 OR ((triple1) -> rule8) OR ((triple2) -> rule2) OR ((((triple5 triple4) -> rule5)) -> rule8))] Charlie is blue.[(triple7)] Charlie is furry.[(triple8)] Charlie is quiet.[(triple9)] Dave is big.[(triple10 OR ((triple14 triple13) -> rule5))] Dave is blue.[(triple11)] Dave is furry.[(triple12)] Dave is nice.[(triple13)] Dave is quiet.[(triple14)] Dave is rough.[(triple15 OR ((triple10) -> rule8) OR ((((triple14 triple13) -> rule5)) -> rule8))] @1: Bob is blue.[(((triple1 triple2) -> rule1) OR ((triple6 triple2) -> rule6) OR ((((triple1) -> rule8) triple2) -> rule6) OR ((((triple2) -> rule2) triple2) -> rule6) OR ((((triple5 triple4) -> rule5) triple2) -> rule1) OR ((((((triple5 triple4) -> rule5)) -> rule8) triple2) -> rule6))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple5 triple4) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple5 ((((triple6 triple2) -> (rule6 % int3)) triple2) -> (rule4 % int2))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
((triple5 ((((((triple2) -> (rule2 % int4)) triple2) -> (rule6 % int3)) triple2) -> (rule4 % int2))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
int4
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
((((triple1 triple2) -> (rule1 % int2)) triple2) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple6 triple2) -> (rule6 % int2)) triple2) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((((triple1) -> (rule8 % int3)) triple2) -> (rule6 % int2)) triple2) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
((((((triple2) -> (rule2 % int3)) triple2) -> (rule6 % int2)) triple2) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
Bob is rough.
("Bob" "is" "rough" "+")
triple6
((triple1) -> (rule8 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple2) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple5 triple4) -> (rule5 % int2))) -> (rule8 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple7
Charlie is furry.
("Charlie" "is" "furry" "+")
triple8
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple9
Dave is big.
("Dave" "is" "big" "+")
triple10
((triple14 triple13) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
triple11
Dave is furry.
("Dave" "is" "furry" "+")
triple12
Dave is nice.
("Dave" "is" "nice" "+")
triple13
Dave is quiet.
("Dave" "is" "quiet" "+")
triple14
Dave is rough.
("Dave" "is" "rough" "+")
triple15
((triple10) -> (rule8 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple14 triple13) -> (rule5 % int2))) -> (rule8 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
((triple1 triple2) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((triple6 triple2) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple1) -> (rule8 % int2)) triple2) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple2) -> (rule2 % int2)) triple2) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple5 triple4) -> (rule5 % int2)) triple2) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((((triple5 triple4) -> (rule5 % int3))) -> (rule8 % int2)) triple2) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3