Anne is nice. Anne is young. Bob is red. Erin is blue. Erin is nice. Erin is quiet. Erin is red. Erin is rough. Erin is smart. Erin is young. If someone is nice then they are red. All young, red people are smart. All smart people are blue.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is red.
("Bob" "is" "red" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
If someone is nice then they are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
All young, red people are smart.
((("someone" "is" "young" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
All smart people are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
Erin is blue.
True
1
proof
[(triple4 OR ((triple9) -> rule3) OR ((((triple10 triple7) -> rule2)) -> rule3) OR ((((triple10 ((triple5) -> rule1)) -> rule2)) -> rule3))]
("Erin" "is" "blue" "+")
triple4
((triple9) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple10 triple7) -> (rule2 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple10 ((triple5) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is not young.
False
1
inv-proof
[(triple10)]
("Erin" "is" "young" "-")
triple10
Anne is red.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "red" "+")
((triple1) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not red.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "red" "-")
((triple1) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
True
4
proof
[(((triple2 ((triple1) -> rule1)) -> rule2))]
("Anne" "is" "smart" "+")
((triple2 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is not smart.
False
4
inv-proof
[(((triple2 ((triple1) -> rule1)) -> rule2))]
("Anne" "is" "smart" "-")
((triple2 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is blue.
True
5
proof
[(((((triple2 ((triple1) -> rule1)) -> rule2)) -> rule3))]
("Anne" "is" "blue" "+")
((((triple2 ((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is not blue.
False
5
inv-proof
[(((((triple2 ((triple1) -> rule1)) -> rule2)) -> rule3))]
("Anne" "is" "blue" "-")
((((triple2 ((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Bob is not blue.
Unknown
inv-rconc
[@2: Bob is blue.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Bob" "is" "blue" "-")
Bob is smart.
Unknown
rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "smart" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Anne is nice.[(triple1)] Anne is young.[(triple2)] Bob is red.[(triple3)] Erin is blue.[(triple4 OR ((triple9) -> rule3) OR ((((triple10 triple7) -> rule2)) -> rule3) OR ((((triple10 ((triple5) -> rule1)) -> rule2)) -> rule3))] Erin is nice.[(triple5)] Erin is quiet.[(triple6)] Erin is red.[(triple7 OR ((triple5) -> rule1))] Erin is rough.[(triple8)] Erin is smart.[(triple9 OR ((triple10 triple7) -> rule2) OR ((triple10 ((triple5) -> rule1)) -> rule2))] Erin is young.[(triple10)] @1: Anne is red.[(((triple1) -> rule1))] @2: Anne is smart.[(((triple2 ((triple1) -> rule1)) -> rule2))] @3: Anne is blue.[(((((triple2 ((triple1) -> rule1)) -> rule2)) -> rule3))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is young.
("Anne" "is" "young" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Erin is blue.
("Erin" "is" "blue" "+")
triple4
((triple9) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple10 triple7) -> (rule2 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple10 ((triple5) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
triple5
Erin is quiet.
("Erin" "is" "quiet" "+")
triple6
Erin is red.
("Erin" "is" "red" "+")
triple7
((triple5) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
triple8
Erin is smart.
("Erin" "is" "smart" "+")
triple9
((triple10 triple7) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple10 ((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
triple10
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((triple2 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
((((triple2 ((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3