Anne is nice. Anne is young. Dave is red. Erin is round. Harry is blue. Harry is nice. Harry is round. All nice people are round. Blue people are young. Kind people are red. All young, nice people are blue. All round, cold people are kind. If someone is red and nice then they are kind. Cold people are kind. If Anne is round and Anne is nice then Anne is red.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is young.
("Anne" "is" "young" "+")
Dave is red.
("Dave" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is round.
("Harry" "is" "round" "+")
All nice people are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
Blue people are young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
Kind people are red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
All young, nice people are blue.
((("someone" "is" "young" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
All round, cold people are kind.
((("someone" "is" "round" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
If someone is red and nice then they are kind.
((("someone" "is" "red" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
Cold people are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
If Anne is round and Anne is nice then Anne is red.
((("Anne" "is" "round" "+") ("Anne" "is" "nice" "+")) -> ("Anne" "is" "red" "+"))
Harry is blue.
True
1
proof
[(triple5)]
("Harry" "is" "blue" "+")
triple5
Anne is not nice.
False
1
inv-proof
[(triple1)]
("Anne" "is" "nice" "-")
triple1
Harry is young.
True
2
proof
[(((triple5) -> rule2))]
("Harry" "is" "young" "+")
((triple5) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is not young.
False
2
inv-proof
[(((triple5) -> rule2))]
("Harry" "is" "young" "-")
((triple5) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Anne is red.
True
4
proof
[(((((triple1) -> rule1) triple1) -> rule8))]
("Anne" "is" "red" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule8 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is not red.
False
4
inv-proof
[(((((triple1) -> rule1) triple1) -> rule8))]
("Anne" "is" "red" "-")
((((triple1) -> (rule1 % int2)) triple1) -> (rule8 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is kind.
True
6
proof
[(((((((triple1) -> rule1) triple1) -> rule8) triple1) -> rule6))]
("Anne" "is" "kind" "+")
((((((triple1) -> (rule1 % int3)) triple1) -> (rule8 % int2)) triple1) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is not kind.
False
6
inv-proof
[(((((((triple1) -> rule1) triple1) -> rule8) triple1) -> rule6))]
("Anne" "is" "kind" "-")
((((((triple1) -> (rule1 % int3)) triple1) -> (rule8 % int2)) triple1) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Dave is not blue.
Unknown
inv-rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "blue" "-")
Dave is round.
Unknown
rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "round" "+")
Dave is not young.
Unknown
inv-rconc
[@2: Dave is young.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Dave" "is" "young" "-")
Erin is blue.
Unknown
rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "blue" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Anne is not cold.
Unknown
inv-random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
@0: Anne is nice.[(triple1)] Anne is young.[(triple2)] Dave is red.[(triple3)] Erin is round.[(triple4)] Harry is blue.[(triple5)] Harry is nice.[(triple6)] Harry is round.[(triple7 OR ((triple6) -> rule1))] @1: Anne is blue.[(((triple2 triple1) -> rule4))] Anne is round.[(((triple1) -> rule1))] Harry is young.[(((triple5) -> rule2))] @2: Anne is red.[(((((triple1) -> rule1) triple1) -> rule8))] @3: Anne is kind.[(((((((triple1) -> rule1) triple1) -> rule8) triple1) -> rule6))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is young.
("Anne" "is" "young" "+")
triple2
Dave is red.
("Dave" "is" "red" "+")
triple3
Erin is round.
("Erin" "is" "round" "+")
triple4
Harry is blue.
("Harry" "is" "blue" "+")
triple5
Harry is nice.
("Harry" "is" "nice" "+")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7
((triple6) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((triple2 triple1) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple5) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule8 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
((((((triple1) -> (rule1 % int3)) triple1) -> (rule8 % int2)) triple1) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3