Anne is white. Bob is cold. Bob is smart. Bob is white. Bob is young. Erin is cold. Erin is green. Erin is kind. Erin is rough. Erin is smart. Erin is white. Erin is young. Gary is green. Gary is kind. Gary is white. Gary is young. All smart, green things are cold. White, kind things are green. If something is white and young then it is kind.
Anne is white.
("Anne" "is" "white" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
All smart, green things are cold.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
White, kind things are green.
((("something" "is" "white" "+") ("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
If something is white and young then it is kind.
((("something" "is" "white" "+") ("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
Erin is young.
True
1
proof
[(triple12)]
("Erin" "is" "young" "+")
triple12
Bob is not cold.
False
1
inv-proof
[(triple2 OR ((triple3 ((triple4 ((triple4 triple5) -> rule3)) -> rule2)) -> rule1))]
("Bob" "is" "cold" "-")
triple2
((triple3 ((triple4 ((triple4 triple5) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is kind.
True
3
proof
[(((triple4 triple5) -> rule3))]
("Bob" "is" "kind" "+")
((triple4 triple5) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not kind.
False
3
inv-proof
[(((triple4 triple5) -> rule3))]
("Bob" "is" "kind" "-")
((triple4 triple5) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is green.
True
5
proof
[(((triple4 ((triple4 triple5) -> rule3)) -> rule2))]
("Bob" "is" "green" "+")
((triple4 ((triple4 triple5) -> (rule3 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is not green.
False
5
inv-proof
[(((triple4 ((triple4 triple5) -> rule3)) -> rule2))]
("Bob" "is" "green" "-")
((triple4 ((triple4 triple5) -> (rule3 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Gary is not cold.
Unknown
inv-rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "cold" "-")
Anne is green.
Unknown
rconc
[@2: Anne is green.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Anne" "is" "green" "+")
Anne is not cold.
Unknown
inv-rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "cold" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
@0: Anne is white.[(triple1)] Bob is cold.[(triple2 OR ((triple3 ((triple4 ((triple4 triple5) -> rule3)) -> rule2)) -> rule1))] Bob is smart.[(triple3)] Bob is white.[(triple4)] Bob is young.[(triple5)] Erin is cold.[(triple6 OR ((triple10 triple7) -> rule1) OR ((triple10 ((triple11 triple8) -> rule2)) -> rule1) OR ((triple10 ((triple11 ((triple11 triple12) -> rule3)) -> rule2)) -> rule1))] Erin is green.[(triple7 OR ((triple11 triple8) -> rule2) OR ((triple11 ((triple11 triple12) -> rule3)) -> rule2))] Erin is kind.[(triple8 OR ((triple11 triple12) -> rule3))] Erin is rough.[(triple9)] Erin is smart.[(triple10)] Erin is white.[(triple11)] Erin is young.[(triple12)] Gary is green.[(triple13 OR ((triple15 triple14) -> rule2) OR ((triple15 ((triple15 triple16) -> rule3)) -> rule2))] Gary is kind.[(triple14 OR ((triple15 triple16) -> rule3))] Gary is white.[(triple15)] Gary is young.[(triple16)] @1: Bob is kind.[(((triple4 triple5) -> rule3))] @2: Bob is green.[(((triple4 ((triple4 triple5) -> rule3)) -> rule2))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
((triple3 ((triple4 ((triple4 triple5) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
Bob is young.
("Bob" "is" "young" "+")
triple5
Erin is cold.
("Erin" "is" "cold" "+")
triple6
((triple10 triple7) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple10 ((triple11 triple8) -> (rule2 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((triple10 ((triple11 ((triple11 triple12) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
triple7
((triple11 triple8) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((triple11 ((triple11 triple12) -> (rule3 % int2))) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
triple8
((triple11 triple12) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
triple9
Erin is smart.
("Erin" "is" "smart" "+")
triple10
Erin is white.
("Erin" "is" "white" "+")
triple11
Erin is young.
("Erin" "is" "young" "+")
triple12
Gary is green.
("Gary" "is" "green" "+")
triple13
((triple15 triple14) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple15 ((triple15 triple16) -> (rule3 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
triple14
((triple15 triple16) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple15
Gary is young.
("Gary" "is" "young" "+")
triple16
Bob is kind.
("Bob" "is" "kind" "+")
((triple4 triple5) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((triple4 ((triple4 triple5) -> (rule3 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2