Charlie is quiet. Charlie is young. Gary is cold. If someone is cold then they are quiet. If someone is young then they are rough. All blue, rough people are cold. Blue, rough people are red. Quiet people are young. If Gary is red then Gary is quiet. If someone is red then they are young. If Gary is rough and Gary is quiet then Gary is white.
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
If someone is cold then they are quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
If someone is young then they are rough.
((("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
All blue, rough people are cold.
((("someone" "is" "blue" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
Blue, rough people are red.
((("someone" "is" "blue" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
Quiet people are young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
If Gary is red then Gary is quiet.
((("Gary" "is" "red" "+")) -> ("Gary" "is" "quiet" "+"))
If someone is red then they are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If Gary is rough and Gary is quiet then Gary is white.
((("Gary" "is" "rough" "+") ("Gary" "is" "quiet" "+")) -> ("Gary" "is" "white" "+"))
Gary is cold.
True
1
proof
[(triple3)]
("Gary" "is" "cold" "+")
triple3
Gary is not cold.
False
1
inv-proof
[(triple3)]
("Gary" "is" "cold" "-")
triple3
Charlie is rough.
True
2
proof
[(((triple2) -> rule2) OR ((((triple1) -> rule5)) -> rule2))]
("Charlie" "is" "rough" "+")
((triple2) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Gary is not quiet.
False
2
inv-proof
[(((triple3) -> rule1))]
("Gary" "is" "quiet" "-")
((triple3) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is young.
True
3
proof
[(((((triple3) -> rule1)) -> rule5))]
("Gary" "is" "young" "+")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not young.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule5))]
("Gary" "is" "young" "-")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is rough.
True
4
proof
[(((((((triple3) -> rule1)) -> rule5)) -> rule2))]
("Gary" "is" "rough" "+")
((((((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is not rough.
False
4
inv-proof
[(((((((triple3) -> rule1)) -> rule5)) -> rule2))]
("Gary" "is" "rough" "-")
((((((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is not red.
Unknown
inv-rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "red" "-")
Charlie is red.
Unknown
rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "red" "+")
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
@0: Charlie is quiet.[(triple1)] Charlie is young.[(triple2 OR ((triple1) -> rule5))] Gary is cold.[(triple3)] @1: Charlie is rough.[(((triple2) -> rule2) OR ((((triple1) -> rule5)) -> rule2))] Gary is quiet.[(((triple3) -> rule1))] @2: Gary is young.[(((((triple3) -> rule1)) -> rule5))] @3: Gary is rough.[(((((((triple3) -> rule1)) -> rule5)) -> rule2))] @4: Gary is white.[(((((((((triple3) -> rule1)) -> rule5)) -> rule2) ((triple3) -> rule1)) -> rule8))]
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple1
Charlie is young.
("Charlie" "is" "young" "+")
triple2
((triple1) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple2) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple3) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
((((((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
((((((((triple3) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule2 % int2)) ((triple3) -> (rule1 % int4))) -> (rule8 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4