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