Dave is blue. Dave is cold. Erin is green. Gary is blue. Gary is cold. Gary is red. Harry is blue. All furry people are cold. Blue people are red. If someone is smart and not green then they are blue. If someone is cold then they are blue. If someone is green then they are furry. If someone is green and red then they are not smart.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is red.
("Gary" "is" "red" "+")
Harry is blue.
("Harry" "is" "blue" "+")
All furry people are cold.
((("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
Blue people are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If someone is smart and not green then they are blue.
((("someone" "is" "smart" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "blue" "+"))
If someone is cold then they are blue.
((("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
If someone is green then they are furry.
((("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
If someone is green and red then they are not smart.
((("someone" "is" "green" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "smart" "-"))
Erin is green.
True
1
proof
[(triple3)]
("Erin" "is" "green" "+")
triple3
Dave is not blue.
False
1
inv-proof
[(triple1 OR ((triple2) -> rule4))]
("Dave" "is" "blue" "-")
triple1
((triple2) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is red.
True
2
proof
[(((triple1) -> rule2) OR ((((triple2) -> rule4)) -> rule2))]
("Dave" "is" "red" "+")
((triple1) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Erin is not furry.
False
2
inv-proof
[(((triple3) -> rule5))]
("Erin" "is" "furry" "-")
((triple3) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
True
3
proof
[(((((triple3) -> rule5)) -> rule1))]
("Erin" "is" "cold" "+")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is not cold.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule1))]
("Erin" "is" "cold" "-")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is blue.
True
4
proof
[(((((((triple3) -> rule5)) -> rule1)) -> rule4))]
("Erin" "is" "blue" "+")
((((((triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is not blue.
False
4
inv-proof
[(((((((triple3) -> rule5)) -> rule1)) -> rule4))]
("Erin" "is" "blue" "-")
((((((triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is red.
True
5
proof
[(((((((((triple3) -> rule5)) -> rule1)) -> rule4)) -> rule2))]
("Erin" "is" "red" "+")
((((((((triple3) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
Erin is not red.
False
5
inv-proof
[(((((((((triple3) -> rule5)) -> rule1)) -> rule4)) -> rule2))]
("Erin" "is" "red" "-")
((((((((triple3) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
Erin is not smart.
True
7
proof
[(((triple3 ((((((((triple3) -> rule5)) -> rule1)) -> rule4)) -> rule2)) -> rule6))]
("Erin" "is" "smart" "-")
((triple3 ((((((((triple3) -> (rule5 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is not smart.
("Erin" "is" "smart" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
Erin is furry.
("Erin" "is" "furry" "+")
int5
Erin is smart.
False
7
inv-proof
[(((triple3 ((((((((triple3) -> rule5)) -> rule1)) -> rule4)) -> rule2)) -> rule6))]
("Erin" "is" "smart" "+")
((triple3 ((((((((triple3) -> (rule5 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is not smart.
("Erin" "is" "smart" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
Erin is furry.
("Erin" "is" "furry" "+")
int5
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "furry" "-")
Harry is furry.
Unknown
rconc
[@1: Harry is furry.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "furry" "+")
Harry is not cold.
Unknown
inv-rconc
[@2: Harry is cold.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Harry" "is" "cold" "-")
Gary is furry.
Unknown
rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "furry" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Dave is blue.[(triple1 OR ((triple2) -> rule4))] Dave is cold.[(triple2)] Erin is green.[(triple3)] Gary is blue.[(triple4 OR ((triple5) -> rule4))] Gary is cold.[(triple5)] Gary is red.[(triple6 OR ((triple4) -> rule2) OR ((((triple5) -> rule4)) -> rule2))] Harry is blue.[(triple7)] @1: Dave is red.[(((triple1) -> rule2) OR ((((triple2) -> rule4)) -> rule2))] Erin is furry.[(((triple3) -> rule5))] Harry is red.[(((triple7) -> rule2))] @2: Erin is cold.[(((((triple3) -> rule5)) -> rule1))] @3: Erin is blue.[(((((((triple3) -> rule5)) -> rule1)) -> rule4))] @4: Erin is red.[(((((((((triple3) -> rule5)) -> rule1)) -> rule4)) -> rule2))] @5: Erin is not smart.[(((triple3 ((((((((triple3) -> rule5)) -> rule1)) -> rule4)) -> rule2)) -> rule6))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
((triple2) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Erin is green.
("Erin" "is" "green" "+")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
triple4
((triple5) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple5
Gary is red.
("Gary" "is" "red" "+")
triple6
((triple4) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple5) -> (rule4 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
triple7
Dave is red.
("Dave" "is" "red" "+")
((triple1) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
((triple3) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple7) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
((((((triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
((((((((triple3) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
Erin is not smart.
("Erin" "is" "smart" "-")
((triple3 ((((((((triple3) -> (rule5 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is not smart.
("Erin" "is" "smart" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
Erin is furry.
("Erin" "is" "furry" "+")
int5