Bob is smart. Bob is young. Dave is quiet. Dave is young. Fiona is nice. Fiona is young. Harry is nice. Rough, nice things are young. Cold things are young. If something is young then it is nice. All nice things are white. Nice, young things are not cold. White things are rough. If Harry is rough and Harry is not cold then Harry is not quiet.
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Rough, nice things are young.
((("something" "is" "rough" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
Cold things are young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
If something is young then it is nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
All nice things are white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
Nice, young things are not cold.
((("something" "is" "nice" "+") ("something" "is" "young" "+")) -> ("something" "is" "cold" "-"))
White things are rough.
((("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
If Harry is rough and Harry is not cold then Harry is not quiet.
((("Harry" "is" "rough" "+") ("Harry" "is" "cold" "~")) -> ("Harry" "is" "quiet" "-"))
Bob is smart.
True
1
proof
[(triple1)]
("Bob" "is" "smart" "+")
triple1
Fiona is not young.
False
1
inv-proof
[(triple6 OR ((((((triple5) -> rule4)) -> rule6) triple5) -> rule1))]
("Fiona" "is" "young" "-")
triple6
((((((triple5) -> (rule4 % int3))) -> (rule6 % int2)) triple5) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is white.
True
2
proof
[(((triple5) -> rule4) OR ((((triple6) -> rule3)) -> rule4))]
("Fiona" "is" "white" "+")
((triple5) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Dave is not nice.
False
2
inv-proof
[(((triple4) -> rule3))]
("Dave" "is" "nice" "-")
((triple4) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Harry is rough.
True
3
proof
[(((((triple7) -> rule4)) -> rule6))]
("Harry" "is" "rough" "+")
((((triple7) -> (rule4 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Dave is cold.
False
4
inv-proof
[(((((triple4) -> rule3) triple4) -> rule5))]
("Dave" "is" "cold" "+")
((((triple4) -> (rule3 % int2)) triple4) -> (rule5 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Harry is young.
True
5
proof
[(((((((triple7) -> rule4)) -> rule6) triple7) -> rule1))]
("Harry" "is" "young" "+")
((((((triple7) -> (rule4 % int3))) -> (rule6 % int2)) triple7) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is not young.
False
5
inv-proof
[(((((((triple7) -> rule4)) -> rule6) triple7) -> rule1))]
("Harry" "is" "young" "-")
((((((triple7) -> (rule4 % int3))) -> (rule6 % int2)) triple7) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is not cold.
True
7
proof
[(((triple7 ((((((triple7) -> rule4)) -> rule6) triple7) -> rule1)) -> rule5))]
("Harry" "is" "cold" "-")
((triple7 ((((((triple7) -> (rule4 % int4))) -> (rule6 % int3)) triple7) -> (rule1 % int2))) -> (rule5 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
Harry is cold.
False
7
inv-proof
[(((triple7 ((((((triple7) -> rule4)) -> rule6) triple7) -> rule1)) -> rule5))]
("Harry" "is" "cold" "+")
((triple7 ((((((triple7) -> (rule4 % int4))) -> (rule6 % int3)) triple7) -> (rule1 % int2))) -> (rule5 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
Harry is not quiet.
True
11
proof
[(((((((triple7) -> rule4)) -> rule6) ((triple7 ((((((triple7) -> rule4)) -> rule6) triple7) -> rule1)) -> rule5)) -> rule7))]
("Harry" "is" "quiet" "-")
((((((triple7) -> (rule4 % int5))) -> (rule6 % int4)) ((triple7 ((((((triple7) -> (rule4 % int5))) -> (rule6 % int4)) triple7) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is not cold.
("Harry" "is" "cold" "-")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is white.
("Harry" "is" "white" "+")
int5
Harry is quiet.
False
11
inv-proof
[(((((((triple7) -> rule4)) -> rule6) ((triple7 ((((((triple7) -> rule4)) -> rule6) triple7) -> rule1)) -> rule5)) -> rule7))]
("Harry" "is" "quiet" "+")
((((((triple7) -> (rule4 % int5))) -> (rule6 % int4)) ((triple7 ((((((triple7) -> (rule4 % int5))) -> (rule6 % int4)) triple7) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is not cold.
("Harry" "is" "cold" "-")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is white.
("Harry" "is" "white" "+")
int5
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
@0: Bob is smart.[(triple1)] Bob is young.[(triple2)] Dave is quiet.[(triple3)] Dave is young.[(triple4)] Fiona is nice.[(triple5 OR ((triple6) -> rule3))] Fiona is young.[(triple6 OR ((((((triple5) -> rule4)) -> rule6) triple5) -> rule1))] Harry is nice.[(triple7)] @1: Bob is nice.[(((triple2) -> rule3))] Dave is nice.[(((triple4) -> rule3))] Fiona is not cold.[(((triple5 triple6) -> rule5) OR ((((triple6) -> rule3) triple6) -> rule5) OR ((triple5 ((((((triple5) -> rule4)) -> rule6) triple5) -> rule1)) -> rule5) OR ((((triple6) -> rule3) ((((((triple5) -> rule4)) -> rule6) triple5) -> rule1)) -> rule5))] Fiona is white.[(((triple5) -> rule4) OR ((((triple6) -> rule3)) -> rule4))] Harry is white.[(((triple7) -> rule4))] @2: Bob is not cold.[(((((triple2) -> rule3) triple2) -> rule5))] Bob is white.[(((((triple2) -> rule3)) -> rule4))] Dave is not cold.[(((((triple4) -> rule3) triple4) -> rule5))] Dave is white.[(((((triple4) -> rule3)) -> rule4))] Fiona is rough.[(((((triple5) -> rule4)) -> rule6) OR ((((((triple6) -> rule3)) -> rule4)) -> rule6))] Harry is rough.[(((((triple7) -> rule4)) -> rule6))] @3: Bob is rough.[(((((((triple2) -> rule3)) -> rule4)) -> rule6))] Dave is rough.[(((((((triple4) -> rule3)) -> rule4)) -> rule6))] Harry is young.[(((((((triple7) -> rule4)) -> rule6) triple7) -> rule1))] @4: Harry is not cold.[(((triple7 ((((((triple7) -> rule4)) -> rule6) triple7) -> rule1)) -> rule5))] @5: Harry is not quiet.[(((((((triple7) -> rule4)) -> rule6) ((triple7 ((((((triple7) -> rule4)) -> rule6) triple7) -> rule1)) -> rule5)) -> rule7))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Dave is young.
("Dave" "is" "young" "+")
triple4
Fiona is nice.
("Fiona" "is" "nice" "+")
triple5
((triple6) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
triple6
((((((triple5) -> (rule4 % int3))) -> (rule6 % int2)) triple5) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
triple7
Bob is nice.
("Bob" "is" "nice" "+")
((triple2) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple4) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Fiona is not cold.
("Fiona" "is" "cold" "-")
((triple5 triple6) -> (rule5 % int1))
Fiona is not cold.
("Fiona" "is" "cold" "-")
int1
((((triple6) -> (rule3 % int2)) triple6) -> (rule5 % int1))
Fiona is not cold.
("Fiona" "is" "cold" "-")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
((triple5 ((((((triple5) -> (rule4 % int4))) -> (rule6 % int3)) triple5) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is not cold.
("Fiona" "is" "cold" "-")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4
((((triple6) -> (rule3 % int5)) ((((((triple5) -> (rule4 % int4))) -> (rule6 % int3)) triple5) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is not cold.
("Fiona" "is" "cold" "-")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4
Fiona is nice.
("Fiona" "is" "nice" "+")
int5
Fiona is white.
("Fiona" "is" "white" "+")
((triple5) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((triple7) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Bob is not cold.
("Bob" "is" "cold" "-")
((((triple2) -> (rule3 % int2)) triple2) -> (rule5 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Dave is not cold.
("Dave" "is" "cold" "-")
((((triple4) -> (rule3 % int2)) triple4) -> (rule5 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((((triple4) -> (rule3 % int2))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
((((triple5) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
((((((triple6) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
((((triple7) -> (rule4 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
((((((triple4) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
((((((triple7) -> (rule4 % int3))) -> (rule6 % int2)) triple7) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is not cold.
("Harry" "is" "cold" "-")
((triple7 ((((((triple7) -> (rule4 % int4))) -> (rule6 % int3)) triple7) -> (rule1 % int2))) -> (rule5 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
Harry is not quiet.
("Harry" "is" "quiet" "-")
((((((triple7) -> (rule4 % int5))) -> (rule6 % int4)) ((triple7 ((((((triple7) -> (rule4 % int5))) -> (rule6 % int4)) triple7) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is not cold.
("Harry" "is" "cold" "-")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is white.
("Harry" "is" "white" "+")
int5