Bob is big. Bob is red. Gary is big. Gary is cold. Gary is red. Harry is blue. Harry is quiet. Blue things are red. If something is big then it is red. All blue, quiet things are big. All nice things are cold. Big things are nice. All blue things are not green. If something is green and red then it is not quiet. Green things are blue.
Bob is big.
("Bob" "is" "big" "+")
Bob is red.
("Bob" "is" "red" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is red.
("Gary" "is" "red" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Blue things are red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
If something is big then it is red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
All blue, quiet things are big.
((("something" "is" "blue" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
All nice things are cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
Big things are nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
All blue things are not green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "-"))
If something is green and red then it is not quiet.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "-"))
Green things are blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
Bob is red.
True
1
proof
[(triple2 OR ((triple1) -> rule2))]
("Bob" "is" "red" "+")
triple2
((triple1) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not big.
False
1
inv-proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
Harry is not green.
True
2
proof
[(((triple6) -> rule6))]
("Harry" "is" "green" "-")
((triple6) -> (rule6 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
Gary is not nice.
False
2
inv-proof
[(((triple3) -> rule5))]
("Gary" "is" "nice" "-")
((triple3) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Harry is nice.
True
4
proof
[(((((triple6 triple7) -> rule3)) -> rule5))]
("Harry" "is" "nice" "+")
((((triple6 triple7) -> (rule3 % int2))) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Bob is not cold.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule4))]
("Bob" "is" "cold" "-")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Harry is cold.
True
5
proof
[(((((((triple6 triple7) -> rule3)) -> rule5)) -> rule4))]
("Harry" "is" "cold" "+")
((((((triple6 triple7) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is not cold.
False
5
inv-proof
[(((((((triple6 triple7) -> rule3)) -> rule5)) -> rule4))]
("Harry" "is" "cold" "-")
((((((triple6 triple7) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "blue" "-")
Gary is blue.
Unknown
rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "blue" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is big.[(triple1)] Bob is red.[(triple2 OR ((triple1) -> rule2))] Gary is big.[(triple3)] Gary is cold.[(triple4 OR ((((triple3) -> rule5)) -> rule4))] Gary is red.[(triple5 OR ((triple3) -> rule2))] Harry is blue.[(triple6)] Harry is quiet.[(triple7)] @1: Bob is nice.[(((triple1) -> rule5))] Gary is nice.[(((triple3) -> rule5))] Harry is big.[(((triple6 triple7) -> rule3))] Harry is not green.[(((triple6) -> rule6))] Harry is red.[(((triple6) -> rule1) OR ((((triple6 triple7) -> rule3)) -> rule2))] @2: Bob is cold.[(((((triple1) -> rule5)) -> rule4))] Harry is nice.[(((((triple6 triple7) -> rule3)) -> rule5))] @3: Harry is cold.[(((((((triple6 triple7) -> rule3)) -> rule5)) -> rule4))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
((triple1) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
triple5
((triple3) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple6
Harry is quiet.
("Harry" "is" "quiet" "+")
triple7
Bob is nice.
("Bob" "is" "nice" "+")
((triple1) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple3) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple6 triple7) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not green.
("Harry" "is" "green" "-")
((triple6) -> (rule6 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple6) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple6 triple7) -> (rule3 % int2))) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((((triple6 triple7) -> (rule3 % int2))) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((((((triple6 triple7) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3