Anne is blue. Anne is nice. Anne is red. Anne is rough. Anne is round. Anne is white. Anne is young. Bob is round. Bob is white. Charlie is blue. Charlie is nice. Charlie is rough. Charlie is round. Charlie is white. Erin is red. Erin is rough. If someone is round then they are white. If someone is round then they are young. All rough people are nice. Red, white people are rough. All rough, round people are red. If Anne is blue and Anne is red then Anne is nice.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
If someone is round then they are white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
If someone is round then they are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
All rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
Red, white people are rough.
((("someone" "is" "red" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
All rough, round people are red.
((("someone" "is" "rough" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
If Anne is blue and Anne is red then Anne is nice.
((("Anne" "is" "blue" "+") ("Anne" "is" "red" "+")) -> ("Anne" "is" "nice" "+"))
Anne is nice.
True
1
proof
[(triple2 OR ((triple4) -> rule3) OR ((triple1 triple3) -> rule6) OR ((((triple3 triple6) -> rule4)) -> rule3) OR ((triple1 ((triple4 triple5) -> rule5)) -> rule6) OR ((((triple3 ((triple5) -> rule1)) -> rule4)) -> rule3))]
("Anne" "is" "nice" "+")
triple2
((triple4) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((triple1 triple3) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((((triple3 triple6) -> (rule4 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((triple1 ((triple4 triple5) -> (rule5 % int2))) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((triple3 ((triple5) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Erin is not red.
False
1
inv-proof
[(triple15)]
("Erin" "is" "red" "-")
triple15
Bob is young.
True
2
proof
[(((triple8) -> rule2))]
("Bob" "is" "young" "+")
((triple8) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not young.
False
2
inv-proof
[(((triple8) -> rule2))]
("Bob" "is" "young" "-")
((triple8) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not rough.
Unknown
inv-rconc
[@2: Bob is rough.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Bob" "is" "rough" "-")
Bob is nice.
Unknown
rconc
[@3: Bob is nice.[CWA. Example of deepest failure = (rule3 <- rule4 <- rule5 <- FAIL)]]
("Bob" "is" "nice" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
@0: Anne is blue.[(triple1)] Anne is nice.[(triple2 OR ((triple4) -> rule3) OR ((triple1 triple3) -> rule6) OR ((((triple3 triple6) -> rule4)) -> rule3) OR ((triple1 ((triple4 triple5) -> rule5)) -> rule6) OR ((((triple3 ((triple5) -> rule1)) -> rule4)) -> rule3))] Anne is red.[(triple3 OR ((triple4 triple5) -> rule5))] Anne is rough.[(triple4 OR ((triple3 triple6) -> rule4) OR ((triple3 ((triple5) -> rule1)) -> rule4))] Anne is round.[(triple5)] Anne is white.[(triple6 OR ((triple5) -> rule1))] Anne is young.[(triple7 OR ((triple5) -> rule2))] Bob is round.[(triple8)] Bob is white.[(triple9 OR ((triple8) -> rule1))] Charlie is blue.[(triple10)] Charlie is nice.[(triple11 OR ((triple12) -> rule3))] Charlie is rough.[(triple12)] Charlie is round.[(triple13)] Charlie is white.[(triple14 OR ((triple13) -> rule1))] Erin is red.[(triple15)] Erin is rough.[(triple16)] @1: Bob is young.[(((triple8) -> rule2))] Charlie is red.[(((triple12 triple13) -> rule5))] Charlie is young.[(((triple13) -> rule2))] Erin is nice.[(((triple16) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
((triple4) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((triple1 triple3) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((((triple3 triple6) -> (rule4 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((triple1 ((triple4 triple5) -> (rule5 % int2))) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((triple3 ((triple5) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
triple3
((triple4 triple5) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
triple4
((triple3 triple6) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple3 ((triple5) -> (rule1 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
triple5
Anne is white.
("Anne" "is" "white" "+")
triple6
((triple5) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple7
((triple5) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple8
Bob is white.
("Bob" "is" "white" "+")
triple9
((triple8) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple10
Charlie is nice.
("Charlie" "is" "nice" "+")
triple11
((triple12) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple12
Charlie is round.
("Charlie" "is" "round" "+")
triple13
Charlie is white.
("Charlie" "is" "white" "+")
triple14
((triple13) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
triple15
Erin is rough.
("Erin" "is" "rough" "+")
triple16
Bob is young.
("Bob" "is" "young" "+")
((triple8) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((triple12 triple13) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple13) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple16) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1