Charlie is green. Charlie is quiet. Charlie is rough. Charlie is round. Gary is blue. Gary is red. Gary is rough. Gary is round. Harry is blue. Harry is green. Harry is quiet. Harry is red. Harry is rough. Harry is round. Harry is white. If Gary is round then Gary is quiet. If someone is blue and green then they are white. All blue, quiet people are green.
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
If Gary is round then Gary is quiet.
((("Gary" "is" "round" "+")) -> ("Gary" "is" "quiet" "+"))
If someone is blue and green then they are white.
((("someone" "is" "blue" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
All blue, quiet people are green.
((("someone" "is" "blue" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
Charlie is quiet.
True
1
proof
[(triple2)]
("Charlie" "is" "quiet" "+")
triple2
Harry is not rough.
False
1
inv-proof
[(triple13)]
("Harry" "is" "rough" "-")
triple13
Gary is quiet.
True
2
proof
[(((triple8) -> rule1))]
("Gary" "is" "quiet" "+")
((triple8) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not quiet.
False
2
inv-proof
[(((triple8) -> rule1))]
("Gary" "is" "quiet" "-")
((triple8) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is green.
True
4
proof
[(((triple5 ((triple8) -> rule1)) -> rule3))]
("Gary" "is" "green" "+")
((triple5 ((triple8) -> (rule1 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not green.
False
4
inv-proof
[(((triple5 ((triple8) -> rule1)) -> rule3))]
("Gary" "is" "green" "-")
((triple5 ((triple8) -> (rule1 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "white" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Charlie is green.[(triple1)] Charlie is quiet.[(triple2)] Charlie is rough.[(triple3)] Charlie is round.[(triple4)] Gary is blue.[(triple5)] Gary is red.[(triple6)] Gary is rough.[(triple7)] Gary is round.[(triple8)] Harry is blue.[(triple9)] Harry is green.[(triple10 OR ((triple9 triple11) -> rule3))] Harry is quiet.[(triple11)] Harry is red.[(triple12)] Harry is rough.[(triple13)] Harry is round.[(triple14)] Harry is white.[(triple15 OR ((triple9 triple10) -> rule2) OR ((triple9 ((triple9 triple11) -> rule3)) -> rule2))] @1: Gary is quiet.[(((triple8) -> rule1))] @2: Gary is green.[(((triple5 ((triple8) -> rule1)) -> rule3))] @3: Gary is white.[(((triple5 ((triple5 ((triple8) -> rule1)) -> rule3)) -> rule2))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
Charlie is round.
("Charlie" "is" "round" "+")
triple4
Gary is blue.
("Gary" "is" "blue" "+")
triple5
Gary is red.
("Gary" "is" "red" "+")
triple6
Gary is rough.
("Gary" "is" "rough" "+")
triple7
Gary is round.
("Gary" "is" "round" "+")
triple8
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is green.
("Harry" "is" "green" "+")
triple10
((triple9 triple11) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is red.
("Harry" "is" "red" "+")
triple12
Harry is rough.
("Harry" "is" "rough" "+")
triple13
Harry is round.
("Harry" "is" "round" "+")
triple14
Harry is white.
("Harry" "is" "white" "+")
triple15
((triple9 triple10) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple9 ((triple9 triple11) -> (rule3 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple8) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple5 ((triple8) -> (rule1 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((triple5 ((triple5 ((triple8) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3