Anne is smart. Bob is red. All red things are cold. If something is quiet then it is cold. If Anne is blue and Anne is smart then Anne is rough. Quiet things are red. Red, quiet things are nice. All cold things are nice. If Anne is smart then Anne is red. All blue things are quiet.
Anne is smart.
("Anne" "is" "smart" "+")
Bob is red.
("Bob" "is" "red" "+")
All red things are cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If something is quiet then it is cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
If Anne is blue and Anne is smart then Anne is rough.
((("Anne" "is" "blue" "+") ("Anne" "is" "smart" "+")) -> ("Anne" "is" "rough" "+"))
Quiet things are red.
((("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
Red, quiet things are nice.
((("something" "is" "red" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
All cold things are nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If Anne is smart then Anne is red.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "red" "+"))
All blue things are quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
Bob is red.
True
1
proof
[(triple2)]
("Bob" "is" "red" "+")
triple2
Bob is not red.
False
1
inv-proof
[(triple2)]
("Bob" "is" "red" "-")
triple2
Anne is red.
True
2
proof
[(((triple1) -> rule7))]
("Anne" "is" "red" "+")
((triple1) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Bob is not cold.
False
2
inv-proof
[(((triple2) -> rule1))]
("Bob" "is" "cold" "-")
((triple2) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Anne is cold.
True
3
proof
[(((((triple1) -> rule7)) -> rule1))]
("Anne" "is" "cold" "+")
((((triple1) -> (rule7 % int2))) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is not cold.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule1))]
("Anne" "is" "cold" "-")
((((triple1) -> (rule7 % int2))) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is nice.
True
4
proof
[(((((((triple1) -> rule7)) -> rule1)) -> rule6))]
("Anne" "is" "nice" "+")
((((((triple1) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is not nice.
False
4
inv-proof
[(((((((triple1) -> rule7)) -> rule1)) -> rule6))]
("Anne" "is" "nice" "-")
((((((triple1) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Anne" "is" "quiet" "-")
Bob is quiet.
Unknown
rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "quiet" "+")
Anne is not rough.
Unknown
inv-rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "rough" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Anne is smart.[(triple1)] Bob is red.[(triple2)] @1: Anne is red.[(((triple1) -> rule7))] Bob is cold.[(((triple2) -> rule1))] @2: Anne is cold.[(((((triple1) -> rule7)) -> rule1))] Bob is nice.[(((((triple2) -> rule1)) -> rule6))] @3: Anne is nice.[(((((((triple1) -> rule7)) -> rule1)) -> rule6))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((triple2) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((((triple1) -> (rule7 % int2))) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
((((((triple1) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3