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