Anne is kind. Bob is red. Bob is smart. All red people are quiet. If someone is kind then they are quiet. If Bob is cold then Bob is red. Smart, round people are blue. All cold people are blue. If Bob is quiet then Bob is round.
Anne is kind.
("Anne" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
All red people are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
If someone is kind then they are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
If Bob is cold then Bob is red.
((("Bob" "is" "cold" "+")) -> ("Bob" "is" "red" "+"))
Smart, round people are blue.
((("someone" "is" "smart" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
All cold people are blue.
((("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
If Bob is quiet then Bob is round.
((("Bob" "is" "quiet" "+")) -> ("Bob" "is" "round" "+"))
Anne is kind.
True
1
proof
[(triple1)]
("Anne" "is" "kind" "+")
triple1
Bob is not red.
False
1
inv-proof
[(triple2)]
("Bob" "is" "red" "-")
triple2
Bob is quiet.
True
2
proof
[(((triple2) -> rule1))]
("Bob" "is" "quiet" "+")
((triple2) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not quiet.
False
2
inv-proof
[(((triple2) -> rule1))]
("Bob" "is" "quiet" "-")
((triple2) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
True
3
proof
[(((((triple2) -> rule1)) -> rule6))]
("Bob" "is" "round" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is not round.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule6))]
("Bob" "is" "round" "-")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is blue.
True
5
proof
[(((triple3 ((((triple2) -> rule1)) -> rule6)) -> rule4))]
("Bob" "is" "blue" "+")
((triple3 ((((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is not blue.
False
5
inv-proof
[(((triple3 ((((triple2) -> rule1)) -> rule6)) -> rule4))]
("Bob" "is" "blue" "-")
((triple3 ((((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "blue" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is kind.[(triple1)] Bob is red.[(triple2)] Bob is smart.[(triple3)] @1: Anne is quiet.[(((triple1) -> rule2))] Bob is quiet.[(((triple2) -> rule1))] @2: Bob is round.[(((((triple2) -> rule1)) -> rule6))] @3: Bob is blue.[(((triple3 ((((triple2) -> rule1)) -> rule6)) -> rule4))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple2) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
((triple3 ((((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3