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