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