Bob is cold. Bob is furry. Bob is green. Bob is nice. Bob is rough. Dave is nice. Dave is quiet. Dave is red. Dave is rough. Gary is cold. Gary is green. Gary is quiet. If something is quiet then it is red. Cold, quiet things are rough. Rough things are furry. Quiet things are cold. All cold, nice things are rough. Furry, green things are nice.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
If something is quiet then it is red.
((("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
Cold, quiet things are rough.
((("something" "is" "cold" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
Rough things are furry.
((("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
Quiet things are cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
All cold, nice things are rough.
((("something" "is" "cold" "+") ("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
Furry, green things are nice.
((("something" "is" "furry" "+") ("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
Gary is quiet.
True
1
proof
[(triple12)]
("Gary" "is" "quiet" "+")
triple12
Bob is not rough.
False
1
inv-proof
[(triple5 OR ((triple1 triple4) -> rule5) OR ((triple1 ((triple2 triple3) -> rule6)) -> rule5))]
("Bob" "is" "rough" "-")
triple5
((triple1 triple4) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple1 ((triple2 triple3) -> (rule6 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Gary is rough.
True
3
proof
[(((triple10 triple12) -> rule2) OR ((((triple12) -> rule4) triple12) -> rule2))]
("Gary" "is" "rough" "+")
((triple10 triple12) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((triple12) -> (rule4 % int2)) triple12) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not rough.
False
3
inv-proof
[(((triple10 triple12) -> rule2) OR ((((triple12) -> rule4) triple12) -> rule2))]
("Gary" "is" "rough" "-")
((triple10 triple12) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((triple12) -> (rule4 % int2)) triple12) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is furry.
True
4
proof
[(((((triple10 triple12) -> rule2)) -> rule3) OR ((((((triple12) -> rule4) triple12) -> rule2)) -> rule3))]
("Gary" "is" "furry" "+")
((((triple10 triple12) -> (rule2 % int2))) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((((triple12) -> (rule4 % int3)) triple12) -> (rule2 % int2))) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is not furry.
False
4
inv-proof
[(((((triple10 triple12) -> rule2)) -> rule3) OR ((((((triple12) -> rule4) triple12) -> rule2)) -> rule3))]
("Gary" "is" "furry" "-")
((((triple10 triple12) -> (rule2 % int2))) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((((triple12) -> (rule4 % int3)) triple12) -> (rule2 % int2))) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is nice.
True
6
proof
[(((((((triple10 triple12) -> rule2)) -> rule3) triple11) -> rule6) OR ((((((((triple12) -> rule4) triple12) -> rule2)) -> rule3) triple11) -> rule6))]
("Gary" "is" "nice" "+")
((((((triple10 triple12) -> (rule2 % int3))) -> (rule3 % int2)) triple11) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
((((((((triple12) -> (rule4 % int4)) triple12) -> (rule2 % int3))) -> (rule3 % int2)) triple11) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
Gary is not nice.
False
6
inv-proof
[(((((((triple10 triple12) -> rule2)) -> rule3) triple11) -> rule6) OR ((((((((triple12) -> rule4) triple12) -> rule2)) -> rule3) triple11) -> rule6))]
("Gary" "is" "nice" "-")
((((((triple10 triple12) -> (rule2 % int3))) -> (rule3 % int2)) triple11) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
((((((((triple12) -> (rule4 % int4)) triple12) -> (rule2 % int3))) -> (rule3 % int2)) triple11) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
Bob is not red.
Unknown
inv-rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "red" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
@0: Bob is cold.[(triple1)] Bob is furry.[(triple2 OR ((triple5) -> rule3) OR ((((triple1 triple4) -> rule5)) -> rule3))] Bob is green.[(triple3)] Bob is nice.[(triple4 OR ((triple2 triple3) -> rule6) OR ((((triple5) -> rule3) triple3) -> rule6))] Bob is rough.[(triple5 OR ((triple1 triple4) -> rule5) OR ((triple1 ((triple2 triple3) -> rule6)) -> rule5))] Dave is nice.[(triple6)] Dave is quiet.[(triple7)] Dave is red.[(triple8 OR ((triple7) -> rule1))] Dave is rough.[(triple9 OR ((((triple7) -> rule4) triple6) -> rule5) OR ((((triple7) -> rule4) triple7) -> rule2))] Gary is cold.[(triple10 OR ((triple12) -> rule4))] Gary is green.[(triple11)] Gary is quiet.[(triple12)] @1: Dave is cold.[(((triple7) -> rule4))] Dave is furry.[(((triple9) -> rule3) OR ((((((triple7) -> rule4) triple6) -> rule5)) -> rule3) OR ((((((triple7) -> rule4) triple7) -> rule2)) -> rule3))] Gary is red.[(((triple12) -> rule1))] Gary is rough.[(((triple10 triple12) -> rule2) OR ((((triple12) -> rule4) triple12) -> rule2))] @2: Gary is furry.[(((((triple10 triple12) -> rule2)) -> rule3) OR ((((((triple12) -> rule4) triple12) -> rule2)) -> rule3))] @3: Gary is nice.[(((((((triple10 triple12) -> rule2)) -> rule3) triple11) -> rule6) OR ((((((((triple12) -> rule4) triple12) -> rule2)) -> rule3) triple11) -> rule6))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
((triple5) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple1 triple4) -> (rule5 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
((triple2 triple3) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple5) -> (rule3 % int2)) triple3) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
triple5
((triple1 triple4) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple1 ((triple2 triple3) -> (rule6 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
triple6
Dave is quiet.
("Dave" "is" "quiet" "+")
triple7
Dave is red.
("Dave" "is" "red" "+")
triple8
((triple7) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple9
((((triple7) -> (rule4 % int2)) triple6) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((((triple7) -> (rule4 % int2)) triple7) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
triple10
((triple12) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
triple11
Gary is quiet.
("Gary" "is" "quiet" "+")
triple12
Dave is cold.
("Dave" "is" "cold" "+")
((triple7) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((triple9) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((((triple7) -> (rule4 % int3)) triple6) -> (rule5 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
((((((triple7) -> (rule4 % int3)) triple7) -> (rule2 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
((triple12) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple10 triple12) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((triple12) -> (rule4 % int2)) triple12) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
((((triple10 triple12) -> (rule2 % int2))) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((((triple12) -> (rule4 % int3)) triple12) -> (rule2 % int2))) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
((((((triple10 triple12) -> (rule2 % int3))) -> (rule3 % int2)) triple11) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
((((((((triple12) -> (rule4 % int4)) triple12) -> (rule2 % int3))) -> (rule3 % int2)) triple11) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4