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