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