Bob is big. Bob is furry. Bob is rough. Bob is round. Erin is big. Erin is cold. Erin is quiet. Erin is rough. Erin is round. Harry is big. Harry is blue. Harry is cold. Harry is furry. Harry is quiet. Harry is rough. Harry is round. All rough, cold people are big. If Bob is big and Bob is cold then Bob is blue. If someone is rough then they are furry. All blue, quiet people are cold. All round people are rough. Rough, quiet people are round. If Erin is round and Erin is blue then Erin is big. If someone is quiet and rough then they are furry.
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
All rough, cold people are big.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
If Bob is big and Bob is cold then Bob is blue.
((("Bob" "is" "big" "+") ("Bob" "is" "cold" "+")) -> ("Bob" "is" "blue" "+"))
If someone is rough then they are furry.
((("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
All blue, quiet people are cold.
((("someone" "is" "blue" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
All round people are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
Rough, quiet people are round.
((("someone" "is" "rough" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
If Erin is round and Erin is blue then Erin is big.
((("Erin" "is" "round" "+") ("Erin" "is" "blue" "+")) -> ("Erin" "is" "big" "+"))
If someone is quiet and rough then they are furry.
((("someone" "is" "quiet" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
Harry is big.
True
1
proof
[(triple10 OR ((triple15 triple12) -> rule1) OR ((triple15 ((triple11 triple14) -> rule4)) -> rule1) OR ((((triple16) -> rule5) triple12) -> rule1) OR ((((triple16) -> rule5) ((triple11 triple14) -> rule4)) -> rule1))]
("Harry" "is" "big" "+")
triple10
((triple15 triple12) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple15 ((triple11 triple14) -> (rule4 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple16) -> (rule5 % int2)) triple12) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple16) -> (rule5 % int3)) ((triple11 triple14) -> (rule4 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Bob is not big.
False
1
inv-proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
Erin is furry.
True
2
proof
[(((triple8) -> rule3) OR ((triple7 triple8) -> rule8) OR ((((triple9) -> rule5)) -> rule3) OR ((triple7 ((triple9) -> rule5)) -> rule8))]
("Erin" "is" "furry" "+")
((triple8) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple7 triple8) -> (rule8 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((triple9) -> (rule5 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((triple7 ((triple9) -> (rule5 % int2))) -> (rule8 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is not furry.
False
2
inv-proof
[(((triple8) -> rule3) OR ((triple7 triple8) -> rule8) OR ((((triple9) -> rule5)) -> rule3) OR ((triple7 ((triple9) -> rule5)) -> rule8))]
("Erin" "is" "furry" "-")
((triple8) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple7 triple8) -> (rule8 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((triple9) -> (rule5 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((triple7 ((triple9) -> (rule5 % int2))) -> (rule8 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "cold" "-")
Bob is blue.
Unknown
rconc
[@2: Bob is blue.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Bob" "is" "blue" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is big.[(triple1)] Bob is furry.[(triple2 OR ((triple3) -> rule3) OR ((((triple4) -> rule5)) -> rule3))] Bob is rough.[(triple3 OR ((triple4) -> rule5))] Bob is round.[(triple4)] Erin is big.[(triple5 OR ((triple8 triple6) -> rule1) OR ((((triple9) -> rule5) triple6) -> rule1))] Erin is cold.[(triple6)] Erin is quiet.[(triple7)] Erin is rough.[(triple8 OR ((triple9) -> rule5))] Erin is round.[(triple9 OR ((triple8 triple7) -> rule6))] Harry is big.[(triple10 OR ((triple15 triple12) -> rule1) OR ((triple15 ((triple11 triple14) -> rule4)) -> rule1) OR ((((triple16) -> rule5) triple12) -> rule1) OR ((((triple16) -> rule5) ((triple11 triple14) -> rule4)) -> rule1))] Harry is blue.[(triple11)] Harry is cold.[(triple12 OR ((triple11 triple14) -> rule4))] Harry is furry.[(triple13 OR ((triple15) -> rule3) OR ((triple14 triple15) -> rule8) OR ((((triple16) -> rule5)) -> rule3) OR ((triple14 ((triple16) -> rule5)) -> rule8))] Harry is quiet.[(triple14)] Harry is rough.[(triple15 OR ((triple16) -> rule5))] Harry is round.[(triple16 OR ((triple15 triple14) -> rule6))] @1: Erin is furry.[(((triple8) -> rule3) OR ((triple7 triple8) -> rule8) OR ((((triple9) -> rule5)) -> rule3) OR ((triple7 ((triple9) -> rule5)) -> rule8))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
((triple3) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple4) -> (rule5 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
((triple4) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple4
Erin is big.
("Erin" "is" "big" "+")
triple5
((triple8 triple6) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple9) -> (rule5 % int2)) triple6) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
triple6
Erin is quiet.
("Erin" "is" "quiet" "+")
triple7
Erin is rough.
("Erin" "is" "rough" "+")
triple8
((triple9) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple9
((triple8 triple7) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple10
((triple15 triple12) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple15 ((triple11 triple14) -> (rule4 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple16) -> (rule5 % int2)) triple12) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple16) -> (rule5 % int3)) ((triple11 triple14) -> (rule4 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
triple11
Harry is cold.
("Harry" "is" "cold" "+")
triple12
((triple11 triple14) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple13
((triple15) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple14 triple15) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple16) -> (rule5 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((triple14 ((triple16) -> (rule5 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple14
Harry is rough.
("Harry" "is" "rough" "+")
triple15
((triple16) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple16
((triple15 triple14) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple8) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple7 triple8) -> (rule8 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((triple9) -> (rule5 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((triple7 ((triple9) -> (rule5 % int2))) -> (rule8 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2