Gary is furry. Harry is furry. If someone is quiet and rough then they are cold. Quiet, round people are cold. All furry people are cold. If someone is round and blue then they are cold. Furry, cold people are round. If someone is quiet then they are round. Round people are blue. Blue people are white.
Gary is furry.
("Gary" "is" "furry" "+")
Harry is furry.
("Harry" "is" "furry" "+")
If someone is quiet and rough then they are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
Quiet, round people are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
All furry people are cold.
((("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
If someone is round and blue then they are cold.
((("someone" "is" "round" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
Furry, cold people are round.
((("someone" "is" "furry" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If someone is quiet then they are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
Round people are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
Blue people are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
Gary is furry.
True
1
proof
[(triple1)]
("Gary" "is" "furry" "+")
triple1
Gary is not furry.
False
1
inv-proof
[(triple1)]
("Gary" "is" "furry" "-")
triple1
Gary is cold.
True
2
proof
[(((triple1) -> rule3))]
("Gary" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not cold.
False
2
inv-proof
[(((triple1) -> rule3))]
("Gary" "is" "cold" "-")
((triple1) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Harry is round.
True
4
proof
[(((triple2 ((triple2) -> rule3)) -> rule5))]
("Harry" "is" "round" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not round.
False
4
inv-proof
[(((triple2 ((triple2) -> rule3)) -> rule5))]
("Harry" "is" "round" "-")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is blue.
True
5
proof
[(((((triple2 ((triple2) -> rule3)) -> rule5)) -> rule7))]
("Harry" "is" "blue" "+")
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Gary is not blue.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule3)) -> rule5)) -> rule7))]
("Gary" "is" "blue" "-")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
@0: Gary is furry.[(triple1)] Harry is furry.[(triple2)] @1: Gary is cold.[(((triple1) -> rule3))] Harry is cold.[(((triple2) -> rule3))] @2: Gary is round.[(((triple1 ((triple1) -> rule3)) -> rule5))] Harry is round.[(((triple2 ((triple2) -> rule3)) -> rule5))] @3: Gary is blue.[(((((triple1 ((triple1) -> rule3)) -> rule5)) -> rule7))] Harry is blue.[(((((triple2 ((triple2) -> rule3)) -> rule5)) -> rule7))] @4: Gary is white.[(((((((triple1 ((triple1) -> rule3)) -> rule5)) -> rule7)) -> rule8))] Harry is white.[(((((((triple2 ((triple2) -> rule3)) -> rule5)) -> rule7)) -> rule8))]
Gary is furry.
("Gary" "is" "furry" "+")
triple1
Harry is furry.
("Harry" "is" "furry" "+")
triple2
Gary is cold.
("Gary" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple2) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
((((((triple1 ((triple1) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
Harry is white.
("Harry" "is" "white" "+")
((((((triple2 ((triple2) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4