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