Gary is furry. Harry is furry. Harry is round. If something is cold then it is furry. If something is red then it is green. Young things are green. All furry things are red. Red things are not young. All green things are round.
Gary is furry.
("Gary" "is" "furry" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is round.
("Harry" "is" "round" "+")
If something is cold then it is furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
If something is red then it is green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
Young things are green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
All furry things are red.
((("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
Red things are not young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "-"))
All green things are round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
Gary is furry.
True
1
proof
[(triple1)]
("Gary" "is" "furry" "+")
triple1
Harry is not round.
False
1
inv-proof
[(triple3 OR ((((((triple2) -> rule4)) -> rule2)) -> rule6))]
("Harry" "is" "round" "-")
triple3
((((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is red.
True
2
proof
[(((triple2) -> rule4))]
("Harry" "is" "red" "+")
((triple2) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is not red.
False
2
inv-proof
[(((triple2) -> rule4))]
("Harry" "is" "red" "-")
((triple2) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is not young.
True
3
proof
[(((((triple2) -> rule4)) -> rule5))]
("Harry" "is" "young" "-")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is not green.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule2))]
("Harry" "is" "green" "-")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Gary is round.
True
4
proof
[(((((((triple1) -> rule4)) -> rule2)) -> rule6))]
("Gary" "is" "round" "+")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is not round.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule2)) -> rule6))]
("Gary" "is" "round" "-")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
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)] Harry is round.[(triple3 OR ((((((triple2) -> rule4)) -> rule2)) -> rule6))] @1: Gary is red.[(((triple1) -> rule4))] Harry is red.[(((triple2) -> rule4))] @2: Gary is green.[(((((triple1) -> rule4)) -> rule2))] Gary is not young.[(((((triple1) -> rule4)) -> rule5))] Harry is green.[(((((triple2) -> rule4)) -> rule2))] Harry is not young.[(((((triple2) -> rule4)) -> rule5))] @3: Gary is round.[(((((((triple1) -> rule4)) -> rule2)) -> rule6))]
Gary is furry.
("Gary" "is" "furry" "+")
triple1
Harry is furry.
("Harry" "is" "furry" "+")
triple2
Harry is round.
("Harry" "is" "round" "+")
triple3
((((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
((triple1) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple2) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not young.
("Gary" "is" "young" "-")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Gary is not young.
("Gary" "is" "young" "-")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is not young.
("Harry" "is" "young" "-")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3