Bob is cold. Gary is nice. Gary is red. Harry is cold. Harry is nice. Harry is rough. Harry is round. If Gary is red and Gary is round then Gary is cold. All rough, cold things are young. If Harry is round then Harry is rough. If something is white and nice then it is red. If Harry is white then Harry is cold. If Gary is round then Gary is young. If something is red then it is rough. Cold things are red.
Bob is cold.
("Bob" "is" "cold" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
If Gary is red and Gary is round then Gary is cold.
((("Gary" "is" "red" "+") ("Gary" "is" "round" "+")) -> ("Gary" "is" "cold" "+"))
All rough, cold things are young.
((("something" "is" "rough" "+") ("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
If Harry is round then Harry is rough.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "rough" "+"))
If something is white and nice then it is red.
((("something" "is" "white" "+") ("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If Harry is white then Harry is cold.
((("Harry" "is" "white" "+")) -> ("Harry" "is" "cold" "+"))
If Gary is round then Gary is young.
((("Gary" "is" "round" "+")) -> ("Gary" "is" "young" "+"))
If something is red then it is rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
Cold things are red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
Gary is red.
True
1
proof
[(triple3)]
("Gary" "is" "red" "+")
triple3
Gary is not nice.
False
1
inv-proof
[(triple2)]
("Gary" "is" "nice" "-")
triple2
Bob is red.
True
2
proof
[(((triple1) -> rule8))]
("Bob" "is" "red" "+")
((triple1) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Harry is not red.
False
2
inv-proof
[(((triple4) -> rule8))]
("Harry" "is" "red" "-")
((triple4) -> (rule8 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Bob is rough.
True
3
proof
[(((((triple1) -> rule8)) -> rule7))]
("Bob" "is" "rough" "+")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is not rough.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule7))]
("Bob" "is" "rough" "-")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Gary is not young.
Unknown
inv-rconc
[@2: Gary is young.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Gary" "is" "young" "-")
Gary is cold.
Unknown
rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "cold" "+")
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
@0: Bob is cold.[(triple1)] Gary is nice.[(triple2)] Gary is red.[(triple3)] Harry is cold.[(triple4)] Harry is nice.[(triple5)] Harry is rough.[(triple6 OR ((triple7) -> rule3) OR ((((triple4) -> rule8)) -> rule7))] Harry is round.[(triple7)] @1: Bob is red.[(((triple1) -> rule8))] Gary is rough.[(((triple3) -> rule7))] Harry is red.[(((triple4) -> rule8))] Harry is young.[(((triple6 triple4) -> rule2) OR ((((triple7) -> rule3) triple4) -> rule2) OR ((((((triple4) -> rule8)) -> rule7) triple4) -> rule2))] @2: Bob is rough.[(((((triple1) -> rule8)) -> rule7))] @3: Bob is young.[(((((((triple1) -> rule8)) -> rule7) triple1) -> rule2))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Gary is nice.
("Gary" "is" "nice" "+")
triple2
Gary is red.
("Gary" "is" "red" "+")
triple3
Harry is cold.
("Harry" "is" "cold" "+")
triple4
Harry is nice.
("Harry" "is" "nice" "+")
triple5
Harry is rough.
("Harry" "is" "rough" "+")
triple6
((triple7) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple4) -> (rule8 % int2))) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
triple7
Bob is red.
("Bob" "is" "red" "+")
((triple1) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple3) -> (rule7 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple4) -> (rule8 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple6 triple4) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((triple7) -> (rule3 % int2)) triple4) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((((triple4) -> (rule8 % int3))) -> (rule7 % int2)) triple4) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((((((triple1) -> (rule8 % int3))) -> (rule7 % int2)) triple1) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3