Bob is cold. Bob is green. Bob is nice. Bob is red. Bob is white. Bob is young. Erin is white. Young things are red. All cold, white things are young. If Erin is nice then Erin is red. Green things are nice. If something is white then it is cold. If Erin is nice and Erin is smart then Erin is young.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is white.
("Erin" "is" "white" "+")
Young things are red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
All cold, white things are young.
((("something" "is" "cold" "+") ("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
If Erin is nice then Erin is red.
((("Erin" "is" "nice" "+")) -> ("Erin" "is" "red" "+"))
Green things are nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
If something is white then it is cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
If Erin is nice and Erin is smart then Erin is young.
((("Erin" "is" "nice" "+") ("Erin" "is" "smart" "+")) -> ("Erin" "is" "young" "+"))
Bob is green.
True
1
proof
[(triple2)]
("Bob" "is" "green" "+")
triple2
Erin is not white.
False
1
inv-proof
[(triple7)]
("Erin" "is" "white" "-")
triple7
Erin is cold.
True
2
proof
[(((triple7) -> rule5))]
("Erin" "is" "cold" "+")
((triple7) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is not cold.
False
2
inv-proof
[(((triple7) -> rule5))]
("Erin" "is" "cold" "-")
((triple7) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is young.
True
4
proof
[(((((triple7) -> rule5) triple7) -> rule2))]
("Erin" "is" "young" "+")
((((triple7) -> (rule5 % int2)) triple7) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is not young.
False
4
inv-proof
[(((((triple7) -> rule5) triple7) -> rule2))]
("Erin" "is" "young" "-")
((((triple7) -> (rule5 % int2)) triple7) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is red.
True
5
proof
[(((((((triple7) -> rule5) triple7) -> rule2)) -> rule1))]
("Erin" "is" "red" "+")
((((((triple7) -> (rule5 % int3)) triple7) -> (rule2 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is not red.
False
5
inv-proof
[(((((((triple7) -> rule5) triple7) -> rule2)) -> rule1))]
("Erin" "is" "red" "-")
((((((triple7) -> (rule5 % int3)) triple7) -> (rule2 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is not nice.
Unknown
inv-rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "nice" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
@0: Bob is cold.[(triple1 OR ((triple5) -> rule5))] Bob is green.[(triple2)] Bob is nice.[(triple3 OR ((triple2) -> rule4))] Bob is red.[(triple4 OR ((triple6) -> rule1) OR ((((triple1 triple5) -> rule2)) -> rule1) OR ((((((triple5) -> rule5) triple5) -> rule2)) -> rule1))] Bob is white.[(triple5)] Bob is young.[(triple6 OR ((triple1 triple5) -> rule2) OR ((((triple5) -> rule5) triple5) -> rule2))] Erin is white.[(triple7)] @1: Erin is cold.[(((triple7) -> rule5))] @2: Erin is young.[(((((triple7) -> rule5) triple7) -> rule2))] @3: Erin is red.[(((((((triple7) -> rule5) triple7) -> rule2)) -> rule1))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
((triple5) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
((triple2) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple4
((triple6) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple1 triple5) -> (rule2 % int2))) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((((triple5) -> (rule5 % int3)) triple5) -> (rule2 % int2))) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
triple5
Bob is young.
("Bob" "is" "young" "+")
triple6
((triple1 triple5) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((((triple5) -> (rule5 % int2)) triple5) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
triple7
Erin is cold.
("Erin" "is" "cold" "+")
((triple7) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((((triple7) -> (rule5 % int2)) triple7) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((((((triple7) -> (rule5 % int3)) triple7) -> (rule2 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3