Anne is big. Anne is blue. Anne is furry. Anne is red. Anne is rough. Anne is round. Anne is smart. Charlie is big. Charlie is blue. Gary is big. Gary is blue. Gary is furry. Harry is red. Harry is rough. Harry is smart. If something is furry then it is red. If Harry is rough and Harry is blue then Harry is smart. All big, blue things are red. If something is smart and furry then it is red. If Anne is big then Anne is red. Rough, smart things are furry. Smart, round things are furry. If Anne is blue and Anne is red then Anne is big.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If something is furry then it is red.
((("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
If Harry is rough and Harry is blue then Harry is smart.
((("Harry" "is" "rough" "+") ("Harry" "is" "blue" "+")) -> ("Harry" "is" "smart" "+"))
All big, blue things are red.
((("something" "is" "big" "+") ("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
If something is smart and furry then it is red.
((("something" "is" "smart" "+") ("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
If Anne is big then Anne is red.
((("Anne" "is" "big" "+")) -> ("Anne" "is" "red" "+"))
Rough, smart things are furry.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
Smart, round things are furry.
((("something" "is" "smart" "+") ("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
If Anne is blue and Anne is red then Anne is big.
((("Anne" "is" "blue" "+") ("Anne" "is" "red" "+")) -> ("Anne" "is" "big" "+"))
Gary is furry.
True
1
proof
[(triple12)]
("Gary" "is" "furry" "+")
triple12
Anne is not blue.
False
1
inv-proof
[(triple2)]
("Anne" "is" "blue" "-")
triple2
Charlie is not furry.
Unknown
inv-rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "furry" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Anne is big.[(triple1 OR ((triple2 triple4) -> rule8) OR ((triple2 ((triple3) -> rule1)) -> rule8) OR ((triple2 ((triple7 triple3) -> rule4)) -> rule8) OR ((triple2 ((((triple5 triple7) -> rule6)) -> rule1)) -> rule8) OR ((triple2 ((((triple7 triple6) -> rule7)) -> rule1)) -> rule8) OR ((triple2 ((triple7 ((triple5 triple7) -> rule6)) -> rule4)) -> rule8) OR ((triple2 ((triple7 ((triple7 triple6) -> rule7)) -> rule4)) -> rule8))] Anne is blue.[(triple2)] Anne is furry.[(triple3 OR ((triple5 triple7) -> rule6) OR ((triple7 triple6) -> rule7))] Anne is red.[(triple4 OR ((triple1) -> rule5) OR ((triple3) -> rule1) OR ((triple1 triple2) -> rule3) OR ((triple7 triple3) -> rule4) OR ((((triple5 triple7) -> rule6)) -> rule1) OR ((((triple7 triple6) -> rule7)) -> rule1) OR ((triple7 ((triple5 triple7) -> rule6)) -> rule4) OR ((triple7 ((triple7 triple6) -> rule7)) -> rule4))] Anne is rough.[(triple5)] Anne is round.[(triple6)] Anne is smart.[(triple7)] Charlie is big.[(triple8)] Charlie is blue.[(triple9)] Gary is big.[(triple10)] Gary is blue.[(triple11)] Gary is furry.[(triple12)] Harry is red.[(triple13 OR ((((triple14 triple15) -> rule6)) -> rule1) OR ((triple15 ((triple14 triple15) -> rule6)) -> rule4))] Harry is rough.[(triple14)] Harry is smart.[(triple15)] @1: Charlie is red.[(((triple8 triple9) -> rule3))] Gary is red.[(((triple12) -> rule1) OR ((triple10 triple11) -> rule3))] Harry is furry.[(((triple14 triple15) -> rule6))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple2 triple4) -> (rule8 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((triple2 ((triple3) -> (rule1 % int2))) -> (rule8 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((triple2 ((triple7 triple3) -> (rule4 % int2))) -> (rule8 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((triple2 ((((triple5 triple7) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
((triple2 ((((triple7 triple6) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
((triple2 ((triple7 ((triple5 triple7) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
((triple2 ((triple7 ((triple7 triple6) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is furry.
("Anne" "is" "furry" "+")
triple3
((triple5 triple7) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((triple7 triple6) -> (rule7 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple4
((triple1) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple3) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple1 triple2) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple7 triple3) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple5 triple7) -> (rule6 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((((triple7 triple6) -> (rule7 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((triple7 ((triple5 triple7) -> (rule6 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((triple7 ((triple7 triple6) -> (rule7 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
triple5
Anne is round.
("Anne" "is" "round" "+")
triple6
Anne is smart.
("Anne" "is" "smart" "+")
triple7
Charlie is big.
("Charlie" "is" "big" "+")
triple8
Charlie is blue.
("Charlie" "is" "blue" "+")
triple9
Gary is big.
("Gary" "is" "big" "+")
triple10
Gary is blue.
("Gary" "is" "blue" "+")
triple11
Gary is furry.
("Gary" "is" "furry" "+")
triple12
Harry is red.
("Harry" "is" "red" "+")
triple13
((((triple14 triple15) -> (rule6 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((triple15 ((triple14 triple15) -> (rule6 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
triple14
Harry is smart.
("Harry" "is" "smart" "+")
triple15
Charlie is red.
("Charlie" "is" "red" "+")
((triple8 triple9) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple12) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple10 triple11) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple14 triple15) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1