Charlie is green. Charlie is red. Dave is red. Dave is not round. Dave is white. Dave is not young. Gary is green. Gary is red. Gary is rough. Gary is round. Gary is white. Gary is young. All red things are not quiet. If something is green then it is round. If something is green then it is white. If something is young and not green then it is white. Young things are rough. If something is round and not quiet then it is young.
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is not round.
("Dave" "is" "round" "-")
Dave is white.
("Dave" "is" "white" "+")
Dave is not young.
("Dave" "is" "young" "-")
Gary is green.
("Gary" "is" "green" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
All red things are not quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "-"))
If something is green then it is round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
If something is green then it is white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
If something is young and not green then it is white.
((("something" "is" "young" "+") ("something" "is" "green" "~")) -> ("something" "is" "white" "+"))
Young things are rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
If something is round and not quiet then it is young.
((("something" "is" "round" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "young" "+"))
Gary is red.
True
1
proof
[(triple8)]
("Gary" "is" "red" "+")
triple8
Gary is not green.
False
1
inv-proof
[(triple7)]
("Gary" "is" "green" "-")
triple7
Charlie is round.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "round" "+")
((triple1) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is not round.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "round" "-")
((triple1) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is young.
True
5
proof
[(((((triple1) -> rule2) ((triple2) -> rule1)) -> rule6))]
("Charlie" "is" "young" "+")
((((triple1) -> (rule2 % int3)) ((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is not young.
False
5
inv-proof
[(((((triple1) -> rule2) ((triple2) -> rule1)) -> rule6))]
("Charlie" "is" "young" "-")
((((triple1) -> (rule2 % int3)) ((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is rough.
True
6
proof
[(((((((triple1) -> rule2) ((triple2) -> rule1)) -> rule6)) -> rule5))]
("Charlie" "is" "rough" "+")
((((((triple1) -> (rule2 % int4)) ((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
Charlie is not rough.
False
6
inv-proof
[(((((((triple1) -> rule2) ((triple2) -> rule1)) -> rule6)) -> rule5))]
("Charlie" "is" "rough" "-")
((((((triple1) -> (rule2 % int4)) ((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "rough" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
@0: Charlie is green.[(triple1)] Charlie is red.[(triple2)] Dave is not round.[(triple4)] Dave is not young.[(triple6)] Dave is red.[(triple3)] Dave is white.[(triple5)] Gary is green.[(triple7)] Gary is red.[(triple8)] Gary is rough.[(triple9 OR ((triple12) -> rule5) OR ((((triple10 ((triple8) -> rule1)) -> rule6)) -> rule5) OR ((((((triple7) -> rule2) ((triple8) -> rule1)) -> rule6)) -> rule5))] Gary is round.[(triple10 OR ((triple7) -> rule2))] Gary is white.[(triple11 OR ((triple7) -> rule3))] Gary is young.[(triple12 OR ((triple10 ((triple8) -> rule1)) -> rule6) OR ((((triple7) -> rule2) ((triple8) -> rule1)) -> rule6))] @1: Charlie is not quiet.[(((triple2) -> rule1))] Charlie is round.[(((triple1) -> rule2))] Charlie is white.[(((triple1) -> rule3))] Dave is not quiet.[(((triple3) -> rule1))] Gary is not quiet.[(((triple8) -> rule1))] @2: Charlie is young.[(((((triple1) -> rule2) ((triple2) -> rule1)) -> rule6))] @3: Charlie is rough.[(((((((triple1) -> rule2) ((triple2) -> rule1)) -> rule6)) -> rule5))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Dave is not round.
("Dave" "is" "round" "-")
triple4
Dave is not young.
("Dave" "is" "young" "-")
triple6
Dave is red.
("Dave" "is" "red" "+")
triple3
Dave is white.
("Dave" "is" "white" "+")
triple5
Gary is green.
("Gary" "is" "green" "+")
triple7
Gary is red.
("Gary" "is" "red" "+")
triple8
Gary is rough.
("Gary" "is" "rough" "+")
triple9
((triple12) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((triple10 ((triple8) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is not quiet.
("Gary" "is" "quiet" "-")
int3
((((((triple7) -> (rule2 % int4)) ((triple8) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is not quiet.
("Gary" "is" "quiet" "-")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Gary is round.
("Gary" "is" "round" "+")
triple10
((triple7) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple11
((triple7) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
triple12
((triple10 ((triple8) -> (rule1 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not quiet.
("Gary" "is" "quiet" "-")
int2
((((triple7) -> (rule2 % int3)) ((triple8) -> (rule1 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not quiet.
("Gary" "is" "quiet" "-")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
((triple2) -> (rule1 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple1) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple1) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Dave is not quiet.
("Dave" "is" "quiet" "-")
((triple3) -> (rule1 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Gary is not quiet.
("Gary" "is" "quiet" "-")
((triple8) -> (rule1 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((((triple1) -> (rule2 % int3)) ((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
((((((triple1) -> (rule2 % int4)) ((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4