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