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