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