Dave is blue. Dave is furry. Dave is nice. Dave is quiet. Dave is red. Dave is rough. Dave is round. Gary is red. Harry is blue. Harry is nice. Harry is rough. Harry is round. All round things are nice. Blue things are round. If something is red then it is blue.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Gary is red.
("Gary" "is" "red" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
All round things are nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
Blue things are round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If something is red then it is blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
Dave is red.
True
1
proof
[(triple5)]
("Dave" "is" "red" "+")
triple5
Dave is not rough.
False
1
inv-proof
[(triple6)]
("Dave" "is" "rough" "-")
triple6
Gary is blue.
True
2
proof
[(((triple8) -> rule3))]
("Gary" "is" "blue" "+")
((triple8) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is not blue.
False
2
inv-proof
[(((triple8) -> rule3))]
("Gary" "is" "blue" "-")
((triple8) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
True
3
proof
[(((((triple8) -> rule3)) -> rule2))]
("Gary" "is" "round" "+")
((((triple8) -> (rule3 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is not round.
False
3
inv-proof
[(((((triple8) -> rule3)) -> rule2))]
("Gary" "is" "round" "-")
((((triple8) -> (rule3 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is nice.
True
4
proof
[(((((((triple8) -> rule3)) -> rule2)) -> rule1))]
("Gary" "is" "nice" "+")
((((((triple8) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is not nice.
False
4
inv-proof
[(((((((triple8) -> rule3)) -> rule2)) -> rule1))]
("Gary" "is" "nice" "-")
((((((triple8) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Dave is blue.[(triple1 OR ((triple5) -> rule3))] Dave is furry.[(triple2)] Dave is nice.[(triple3 OR ((triple7) -> rule1) OR ((((triple1) -> rule2)) -> rule1) OR ((((((triple5) -> rule3)) -> rule2)) -> rule1))] Dave is quiet.[(triple4)] Dave is red.[(triple5)] Dave is rough.[(triple6)] Dave is round.[(triple7 OR ((triple1) -> rule2) OR ((((triple5) -> rule3)) -> rule2))] Gary is red.[(triple8)] Harry is blue.[(triple9)] Harry is nice.[(triple10 OR ((triple12) -> rule1) OR ((((triple9) -> rule2)) -> rule1))] Harry is rough.[(triple11)] Harry is round.[(triple12 OR ((triple9) -> rule2))] @1: Gary is blue.[(((triple8) -> rule3))] @2: Gary is round.[(((((triple8) -> rule3)) -> rule2))] @3: Gary is nice.[(((((((triple8) -> rule3)) -> rule2)) -> rule1))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
((triple5) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
((triple7) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((((triple5) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple5
Dave is rough.
("Dave" "is" "rough" "+")
triple6
Dave is round.
("Dave" "is" "round" "+")
triple7
((triple1) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
triple8
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is nice.
("Harry" "is" "nice" "+")
triple10
((triple12) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
triple11
Harry is round.
("Harry" "is" "round" "+")
triple12
((triple9) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple8) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((((triple8) -> (rule3 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((((((triple8) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3