Anne is not cold. Anne is furry. Charlie is furry. Charlie is green. Charlie is red. Charlie is smart. Gary is not cold. Gary is furry. Gary is red. Harry is cold. Harry is furry. Harry is red. If someone is rough then they are round. All smart people are not round. If Harry is green then Harry is not rough. If Anne is smart then Anne is not rough. If Anne is green and Anne is smart then Anne is not round. All smart people are green. All furry people are smart. If someone is red and rough then they are not smart.
Anne is not cold.
("Anne" "is" "cold" "-")
Anne is furry.
("Anne" "is" "furry" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is not cold.
("Gary" "is" "cold" "-")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is red.
("Gary" "is" "red" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is red.
("Harry" "is" "red" "+")
If someone is rough then they are round.
((("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
All smart people are not round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "-"))
If Harry is green then Harry is not rough.
((("Harry" "is" "green" "+")) -> ("Harry" "is" "rough" "-"))
If Anne is smart then Anne is not rough.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "rough" "-"))
If Anne is green and Anne is smart then Anne is not round.
((("Anne" "is" "green" "+") ("Anne" "is" "smart" "+")) -> ("Anne" "is" "round" "-"))
All smart people are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
All furry people are smart.
((("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
If someone is red and rough then they are not smart.
((("someone" "is" "red" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "-"))
Gary is furry.
True
1
proof
[(triple8)]
("Gary" "is" "furry" "+")
triple8
Gary is cold.
False
1
inv-proof
[(triple7)]
("Gary" "is" "cold" "+")
triple7
Charlie is not round.
True
2
proof
[(((triple6) -> rule2) OR ((((triple3) -> rule7)) -> rule2))]
("Charlie" "is" "round" "-")
((triple6) -> (rule2 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
((((triple3) -> (rule7 % int2))) -> (rule2 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Anne is not smart.
False
2
inv-proof
[(((triple2) -> rule7))]
("Anne" "is" "smart" "-")
((triple2) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Harry is green.
True
3
proof
[(((((triple11) -> rule7)) -> rule6))]
("Harry" "is" "green" "+")
((((triple11) -> (rule7 % int2))) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is not green.
False
3
inv-proof
[(((((triple11) -> rule7)) -> rule6))]
("Harry" "is" "green" "-")
((((triple11) -> (rule7 % int2))) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
@0: Anne is furry.[(triple2)] Anne is not cold.[(triple1)] Charlie is furry.[(triple3)] Charlie is green.[(triple4 OR ((triple6) -> rule6) OR ((((triple3) -> rule7)) -> rule6))] Charlie is red.[(triple5)] Charlie is smart.[(triple6 OR ((triple3) -> rule7))] Gary is furry.[(triple8)] Gary is not cold.[(triple7)] Gary is red.[(triple9)] Harry is cold.[(triple10)] Harry is furry.[(triple11)] Harry is red.[(triple12)] @1: Anne is smart.[(((triple2) -> rule7))] Charlie is not round.[(((triple6) -> rule2) OR ((((triple3) -> rule7)) -> rule2))] Gary is smart.[(((triple8) -> rule7))] Harry is smart.[(((triple11) -> rule7))] @2: Anne is green.[(((((triple2) -> rule7)) -> rule6))] Anne is not rough.[(((((triple2) -> rule7)) -> rule4))] Anne is not round.[(((((triple2) -> rule7)) -> rule2) OR ((((((triple2) -> rule7)) -> rule6) ((triple2) -> rule7)) -> rule5))] Gary is green.[(((((triple8) -> rule7)) -> rule6))] Gary is not round.[(((((triple8) -> rule7)) -> rule2))] Harry is green.[(((((triple11) -> rule7)) -> rule6))] Harry is not round.[(((((triple11) -> rule7)) -> rule2))] @3: Harry is not rough.[(((((((triple11) -> rule7)) -> rule6)) -> rule3))]
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is not cold.
("Anne" "is" "cold" "-")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
triple4
((triple6) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((((triple3) -> (rule7 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
triple5
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
((triple3) -> (rule7 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
triple8
Gary is not cold.
("Gary" "is" "cold" "-")
triple7
Gary is red.
("Gary" "is" "red" "+")
triple9
Harry is cold.
("Harry" "is" "cold" "+")
triple10
Harry is furry.
("Harry" "is" "furry" "+")
triple11
Harry is red.
("Harry" "is" "red" "+")
triple12
Anne is smart.
("Anne" "is" "smart" "+")
((triple2) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Charlie is not round.
("Charlie" "is" "round" "-")
((triple6) -> (rule2 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
((((triple3) -> (rule7 % int2))) -> (rule2 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((triple8) -> (rule7 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple11) -> (rule7 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((((triple2) -> (rule7 % int2))) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not rough.
("Anne" "is" "rough" "-")
((((triple2) -> (rule7 % int2))) -> (rule4 % int1))
Anne is not rough.
("Anne" "is" "rough" "-")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not round.
("Anne" "is" "round" "-")
((((triple2) -> (rule7 % int2))) -> (rule2 % int1))
Anne is not round.
("Anne" "is" "round" "-")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((((triple2) -> (rule7 % int3))) -> (rule6 % int2)) ((triple2) -> (rule7 % int3))) -> (rule5 % int1))
Anne is not round.
("Anne" "is" "round" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
((((triple8) -> (rule7 % int2))) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is not round.
("Gary" "is" "round" "-")
((((triple8) -> (rule7 % int2))) -> (rule2 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((((triple11) -> (rule7 % int2))) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is not round.
("Harry" "is" "round" "-")
((((triple11) -> (rule7 % int2))) -> (rule2 % int1))
Harry is not round.
("Harry" "is" "round" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is not rough.
("Harry" "is" "rough" "-")
((((((triple11) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3