Charlie is green. Charlie is rough. Charlie is young. Dave is green. Dave is quiet. Dave is red. Dave is rough. Dave is smart. Dave is young. Erin is rough. If something is quiet and rough then it is young. If something is rough then it is red. All red things are green. If Dave is quiet then Dave is smart. All young things are quiet. Red things are young. Quiet things are rough. All quiet things are green.
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is green.
("Dave" "is" "green" "+")
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 young.
("Dave" "is" "young" "+")
Erin is rough.
("Erin" "is" "rough" "+")
If something is quiet and rough then it is young.
((("something" "is" "quiet" "+") ("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If something is rough then it is red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
All red things are green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If Dave is quiet then Dave is smart.
((("Dave" "is" "quiet" "+")) -> ("Dave" "is" "smart" "+"))
All young things are quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
Red things are young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
Quiet things are rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
All quiet things are green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
Dave is rough.
True
1
proof
[(triple7 OR ((triple5) -> rule7) OR ((((triple9) -> rule5)) -> rule7) OR ((((((triple6) -> rule6)) -> rule5)) -> rule7))]
("Dave" "is" "rough" "+")
triple7
((triple5) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple9) -> (rule5 % int2))) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((((triple6) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Charlie is not rough.
False
1
inv-proof
[(triple2 OR ((((triple3) -> rule5)) -> rule7))]
("Charlie" "is" "rough" "-")
triple2
((((triple3) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is quiet.
True
2
proof
[(((triple3) -> rule5) OR ((((((triple2) -> rule2)) -> rule6)) -> rule5))]
("Charlie" "is" "quiet" "+")
((triple3) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is not quiet.
False
2
inv-proof
[(((triple3) -> rule5) OR ((((((triple2) -> rule2)) -> rule6)) -> rule5))]
("Charlie" "is" "quiet" "-")
((triple3) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Erin is young.
True
3
proof
[(((((triple10) -> rule2)) -> rule6))]
("Erin" "is" "young" "+")
((((triple10) -> (rule2 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is not young.
False
3
inv-proof
[(((((triple10) -> rule2)) -> rule6))]
("Erin" "is" "young" "-")
((((triple10) -> (rule2 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is quiet.
True
4
proof
[(((((((triple10) -> rule2)) -> rule6)) -> rule5))]
("Erin" "is" "quiet" "+")
((((((triple10) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is not quiet.
False
4
inv-proof
[(((((((triple10) -> rule2)) -> rule6)) -> rule5))]
("Erin" "is" "quiet" "-")
((((((triple10) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Charlie is green.[(triple1 OR ((((triple2) -> rule2)) -> rule3) OR ((((triple3) -> rule5)) -> rule8) OR ((((((((triple2) -> rule2)) -> rule6)) -> rule5)) -> rule8) OR ((((((((triple3) -> rule5)) -> rule7)) -> rule2)) -> rule3))] Charlie is rough.[(triple2 OR ((((triple3) -> rule5)) -> rule7))] Charlie is young.[(triple3 OR ((((triple2) -> rule2)) -> rule6))] Dave is green.[(triple4 OR ((triple5) -> rule8) OR ((triple6) -> rule3) OR ((((triple7) -> rule2)) -> rule3) OR ((((triple9) -> rule5)) -> rule8) OR ((((((triple5) -> rule7)) -> rule2)) -> rule3) OR ((((((triple6) -> rule6)) -> rule5)) -> rule8) OR ((((((((triple7) -> rule2)) -> rule6)) -> rule5)) -> rule8) OR ((((((((triple9) -> rule5)) -> rule7)) -> rule2)) -> rule3))] Dave is quiet.[(triple5 OR ((triple9) -> rule5) OR ((((triple6) -> rule6)) -> rule5) OR ((((((triple7) -> rule2)) -> rule6)) -> rule5))] Dave is red.[(triple6 OR ((triple7) -> rule2) OR ((((triple5) -> rule7)) -> rule2) OR ((((((triple9) -> rule5)) -> rule7)) -> rule2))] Dave is rough.[(triple7 OR ((triple5) -> rule7) OR ((((triple9) -> rule5)) -> rule7) OR ((((((triple6) -> rule6)) -> rule5)) -> rule7))] Dave is smart.[(triple8 OR ((triple5) -> rule4) OR ((((triple9) -> rule5)) -> rule4) OR ((((((triple6) -> rule6)) -> rule5)) -> rule4) OR ((((((((triple7) -> rule2)) -> rule6)) -> rule5)) -> rule4))] Dave is young.[(triple9 OR ((triple6) -> rule6) OR ((triple5 triple7) -> rule1) OR ((((triple7) -> rule2)) -> rule6) OR ((triple5 ((triple5) -> rule7)) -> rule1) OR ((((((triple5) -> rule7)) -> rule2)) -> rule6))] Erin is rough.[(triple10)] @1: Charlie is quiet.[(((triple3) -> rule5) OR ((((((triple2) -> rule2)) -> rule6)) -> rule5))] Charlie is red.[(((triple2) -> rule2) OR ((((((triple3) -> rule5)) -> rule7)) -> rule2))] Erin is red.[(((triple10) -> rule2))] @2: Erin is green.[(((((triple10) -> rule2)) -> rule3) OR ((((((((triple10) -> rule2)) -> rule6)) -> rule5)) -> rule8))] Erin is young.[(((((triple10) -> rule2)) -> rule6))] @3: Erin is quiet.[(((((((triple10) -> rule2)) -> rule6)) -> rule5))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((((((triple2) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4
((((((((triple3) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
((((triple3) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
triple3
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
triple4
((triple5) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple6) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((triple9) -> (rule5 % int2))) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((((triple5) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((((triple6) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
((((((((triple7) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
((((((((triple9) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
((triple9) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((((((triple7) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
triple6
((triple7) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple5) -> (rule7 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((((triple9) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
triple7
((triple5) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple9) -> (rule5 % int2))) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((((triple6) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
triple8
((triple5) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((((triple9) -> (rule5 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((((triple6) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
((((((((triple7) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
Dave is young.
("Dave" "is" "young" "+")
triple9
((triple6) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple5 triple7) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((triple5 ((triple5) -> (rule7 % int2))) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((((triple5) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
triple10
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple3) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
((triple2) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((((triple3) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
((triple10) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((((triple10) -> (rule2 % int2))) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((((((triple10) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
int4
Erin is young.
("Erin" "is" "young" "+")
((((triple10) -> (rule2 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
((((((triple10) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3