Charlie is cold. Charlie is rough. Charlie is round. Charlie is young. Dave is big. Dave is cold. Dave is kind. Dave is white. Gary is round. Gary is white. If something is kind then it is big. If something is cold then it is young. All rough, kind things are round. Kind, young things are white. All kind, young things are rough. Big, cold things are round. If something is rough then it is kind. Round things are big.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
If something is kind then it is big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
If something is cold then it is young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
All rough, kind things are round.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
Kind, young things are white.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
All kind, young things are rough.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
Big, cold things are round.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
If something is rough then it is kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
Round things are big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
Charlie is young.
True
1
proof
[(triple4 OR ((triple1) -> rule2))]
("Charlie" "is" "young" "+")
triple4
((triple1) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Dave is not big.
False
1
inv-proof
[(triple5 OR ((triple7) -> rule1) OR ((((((triple7 ((triple6) -> rule2)) -> rule5) triple7) -> rule3)) -> rule8))]
("Dave" "is" "big" "-")
triple5
((triple7) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((((triple7 ((triple6) -> (rule2 % int4))) -> (rule5 % int3)) triple7) -> (rule3 % int2))) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is round.
True
3
proof
[(((triple5 triple6) -> rule6) OR ((((triple7) -> rule1) triple6) -> rule6) OR ((((triple7 ((triple6) -> rule2)) -> rule5) triple7) -> rule3))]
("Dave" "is" "round" "+")
((triple5 triple6) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((triple7) -> (rule1 % int2)) triple6) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((triple7 ((triple6) -> (rule2 % int3))) -> (rule5 % int2)) triple7) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Charlie is not big.
False
2
inv-proof
[(((triple3) -> rule8) OR ((((triple2) -> rule7)) -> rule1) OR ((((triple2 ((triple2) -> rule7)) -> rule3)) -> rule8))]
("Charlie" "is" "big" "-")
((triple3) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple2) -> (rule7 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple2 ((triple2) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Dave is rough.
True
4
proof
[(((triple7 ((triple6) -> rule2)) -> rule5))]
("Dave" "is" "rough" "+")
((triple7 ((triple6) -> (rule2 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Charlie is not white.
False
4
inv-proof
[(((((triple2) -> rule7) triple4) -> rule4) OR ((((triple2) -> rule7) ((triple1) -> rule2)) -> rule4))]
("Charlie" "is" "white" "-")
((((triple2) -> (rule7 % int2)) triple4) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple2) -> (rule7 % int3)) ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Gary is not kind.
Unknown
inv-rconc
[@2: Gary is kind.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("Gary" "is" "kind" "-")
Gary is rough.
Unknown
rconc
[@2: Gary is rough.[CWA. Example of deepest failure = (rule5 <- rule7 <- FAIL)]]
("Gary" "is" "rough" "+")
Gary is not young.
Unknown
inv-rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "young" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
@0: Charlie is cold.[(triple1)] Charlie is rough.[(triple2)] Charlie is round.[(triple3 OR ((triple2 ((triple2) -> rule7)) -> rule3) OR ((((((triple2) -> rule7)) -> rule1) triple1) -> rule6))] Charlie is young.[(triple4 OR ((triple1) -> rule2))] Dave is big.[(triple5 OR ((triple7) -> rule1) OR ((((((triple7 ((triple6) -> rule2)) -> rule5) triple7) -> rule3)) -> rule8))] Dave is cold.[(triple6)] Dave is kind.[(triple7)] Dave is white.[(triple8 OR ((triple7 ((triple6) -> rule2)) -> rule4))] Gary is round.[(triple9)] Gary is white.[(triple10)] @1: Charlie is big.[(((triple3) -> rule8) OR ((((triple2) -> rule7)) -> rule1) OR ((((triple2 ((triple2) -> rule7)) -> rule3)) -> rule8))] Charlie is kind.[(((triple2) -> rule7))] Dave is round.[(((triple5 triple6) -> rule6) OR ((((triple7) -> rule1) triple6) -> rule6) OR ((((triple7 ((triple6) -> rule2)) -> rule5) triple7) -> rule3))] Dave is young.[(((triple6) -> rule2))] Gary is big.[(((triple9) -> rule8))] @2: Charlie is white.[(((((triple2) -> rule7) triple4) -> rule4) OR ((((triple2) -> rule7) ((triple1) -> rule2)) -> rule4))] Dave is rough.[(((triple7 ((triple6) -> rule2)) -> rule5))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
triple3
((triple2 ((triple2) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((((triple2) -> (rule7 % int3))) -> (rule1 % int2)) triple1) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
triple4
((triple1) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
triple5
((triple7) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((((triple7 ((triple6) -> (rule2 % int4))) -> (rule5 % int3)) triple7) -> (rule3 % int2))) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is cold.
("Dave" "is" "cold" "+")
triple6
Dave is kind.
("Dave" "is" "kind" "+")
triple7
Dave is white.
("Dave" "is" "white" "+")
triple8
((triple7 ((triple6) -> (rule2 % int2))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
triple9
Gary is white.
("Gary" "is" "white" "+")
triple10
Charlie is big.
("Charlie" "is" "big" "+")
((triple3) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple2) -> (rule7 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple2 ((triple2) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple2) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple5 triple6) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((triple7) -> (rule1 % int2)) triple6) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((triple7 ((triple6) -> (rule2 % int3))) -> (rule5 % int2)) triple7) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
((triple6) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple9) -> (rule8 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((((triple2) -> (rule7 % int2)) triple4) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple2) -> (rule7 % int3)) ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
((triple7 ((triple6) -> (rule2 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2