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