Anne is round. Anne is white. Bob is cold. Bob is young. Erin is cold. Erin is nice. Erin is white. Fiona is round. Fiona is smart. Fiona is young. If something is kind then it is cold. If Erin is nice then Erin is white. Cold, round things are kind. All round things are cold. If Erin is nice then Erin is cold. Cold things are young.
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If something is kind then it is cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
If Erin is nice then Erin is white.
((("Erin" "is" "nice" "+")) -> ("Erin" "is" "white" "+"))
Cold, round things are kind.
((("something" "is" "cold" "+") ("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
All round things are cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
If Erin is nice then Erin is cold.
((("Erin" "is" "nice" "+")) -> ("Erin" "is" "cold" "+"))
Cold things are young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
Fiona is young.
True
1
proof
[(triple10 OR ((((triple8) -> rule4)) -> rule6))]
("Fiona" "is" "young" "+")
triple10
((((triple8) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Erin is not cold.
False
1
inv-proof
[(triple5 OR ((triple6) -> rule5))]
("Erin" "is" "cold" "-")
triple5
((triple6) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Fiona is cold.
True
2
proof
[(((triple8) -> rule4))]
("Fiona" "is" "cold" "+")
((triple8) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is not cold.
False
2
inv-proof
[(((triple8) -> rule4))]
("Fiona" "is" "cold" "-")
((triple8) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Anne is kind.
True
4
proof
[(((((triple1) -> rule4) triple1) -> rule3))]
("Anne" "is" "kind" "+")
((((triple1) -> (rule4 % int2)) triple1) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is not kind.
False
4
inv-proof
[(((((triple1) -> rule4) triple1) -> rule3))]
("Anne" "is" "kind" "-")
((((triple1) -> (rule4 % int2)) triple1) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Erin is not kind.
Unknown
inv-rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "kind" "-")
Bob is kind.
Unknown
rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "kind" "+")
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Anne is round.[(triple1)] Anne is white.[(triple2)] Bob is cold.[(triple3)] Bob is young.[(triple4 OR ((triple3) -> rule6))] Erin is cold.[(triple5 OR ((triple6) -> rule5))] Erin is nice.[(triple6)] Erin is white.[(triple7 OR ((triple6) -> rule2))] Fiona is round.[(triple8)] Fiona is smart.[(triple9)] Fiona is young.[(triple10 OR ((((triple8) -> rule4)) -> rule6))] @1: Anne is cold.[(((triple1) -> rule4))] Erin is young.[(((triple5) -> rule6) OR ((((triple6) -> rule5)) -> rule6))] Fiona is cold.[(((triple8) -> rule4))] @2: Anne is kind.[(((((triple1) -> rule4) triple1) -> rule3))] Anne is young.[(((((triple1) -> rule4)) -> rule6))] Fiona is kind.[(((((triple8) -> rule4) triple8) -> rule3))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
Bob is cold.
("Bob" "is" "cold" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
((triple3) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
triple5
((triple6) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple6
Erin is white.
("Erin" "is" "white" "+")
triple7
((triple6) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
triple8
Fiona is smart.
("Fiona" "is" "smart" "+")
triple9
Fiona is young.
("Fiona" "is" "young" "+")
triple10
((((triple8) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple5) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple8) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((((triple1) -> (rule4 % int2)) triple1) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
((((triple8) -> (rule4 % int2)) triple8) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2