Charlie is cold. Charlie is quiet. Charlie is red. Dave is cold. Dave is quiet. Dave is red. Dave is rough. Dave is smart. Dave is white. Erin is red. Erin is rough. Erin is smart. If Dave is cold and Dave is rough then Dave is quiet. If Dave is rough then Dave is white. All big people are white. White people are cold. All smart, white people are quiet. All rough people are big.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
If Dave is cold and Dave is rough then Dave is quiet.
((("Dave" "is" "cold" "+") ("Dave" "is" "rough" "+")) -> ("Dave" "is" "quiet" "+"))
If Dave is rough then Dave is white.
((("Dave" "is" "rough" "+")) -> ("Dave" "is" "white" "+"))
All big people are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
White people are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
All smart, white people are quiet.
((("someone" "is" "smart" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
All rough people are big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
Charlie is red.
True
1
proof
[(triple3)]
("Charlie" "is" "red" "+")
triple3
Charlie is not red.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "red" "-")
triple3
Dave is big.
True
2
proof
[(((triple7) -> rule6))]
("Dave" "is" "big" "+")
((triple7) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Erin is not big.
False
2
inv-proof
[(((triple11) -> rule6))]
("Erin" "is" "big" "-")
((triple11) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is white.
True
3
proof
[(((((triple11) -> rule6)) -> rule3))]
("Erin" "is" "white" "+")
((((triple11) -> (rule6 % int2))) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is not white.
False
3
inv-proof
[(((((triple11) -> rule6)) -> rule3))]
("Erin" "is" "white" "-")
((((triple11) -> (rule6 % int2))) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Charlie is not white.
Unknown
inv-rconc
[@2: Charlie is white.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Charlie" "is" "white" "-")
Charlie is big.
Unknown
rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "big" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Charlie is cold.[(triple1)] Charlie is quiet.[(triple2)] Charlie is red.[(triple3)] Dave is cold.[(triple4 OR ((triple9) -> rule4) OR ((((triple7) -> rule2)) -> rule4) OR ((((((triple7) -> rule6)) -> rule3)) -> rule4))] Dave is quiet.[(triple5 OR ((triple4 triple7) -> rule1) OR ((triple8 triple9) -> rule5) OR ((triple8 ((triple7) -> rule2)) -> rule5) OR ((((triple9) -> rule4) triple7) -> rule1) OR ((triple8 ((((triple7) -> rule6)) -> rule3)) -> rule5) OR ((((((triple7) -> rule2)) -> rule4) triple7) -> rule1) OR ((((((((triple7) -> rule6)) -> rule3)) -> rule4) triple7) -> rule1))] Dave is red.[(triple6)] Dave is rough.[(triple7)] Dave is smart.[(triple8)] Dave is white.[(triple9 OR ((triple7) -> rule2) OR ((((triple7) -> rule6)) -> rule3))] Erin is red.[(triple10)] Erin is rough.[(triple11)] Erin is smart.[(triple12)] @1: Dave is big.[(((triple7) -> rule6))] Erin is big.[(((triple11) -> rule6))] @2: Erin is white.[(((((triple11) -> rule6)) -> rule3))] @3: Erin is cold.[(((((((triple11) -> rule6)) -> rule3)) -> rule4))] Erin is quiet.[(((triple12 ((((triple11) -> rule6)) -> rule3)) -> rule5))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple4
((triple9) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((((triple7) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
((triple4 triple7) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple8 triple9) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple8 ((triple7) -> (rule2 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple9) -> (rule4 % int2)) triple7) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((triple8 ((((triple7) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((((((triple7) -> (rule2 % int3))) -> (rule4 % int2)) triple7) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((((((((triple7) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule4 % int2)) triple7) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
triple6
Dave is rough.
("Dave" "is" "rough" "+")
triple7
Dave is smart.
("Dave" "is" "smart" "+")
triple8
Dave is white.
("Dave" "is" "white" "+")
triple9
((triple7) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple7) -> (rule6 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
triple10
Erin is rough.
("Erin" "is" "rough" "+")
triple11
Erin is smart.
("Erin" "is" "smart" "+")
triple12
Dave is big.
("Dave" "is" "big" "+")
((triple7) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple11) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((((triple11) -> (rule6 % int2))) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((((((triple11) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple12 ((((triple11) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3