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