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