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