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