Anne is furry. Anne is kind. Anne is quiet. Anne is red. Charlie is big. Charlie is kind. Charlie is quiet. Charlie is red. Charlie is round. Erin is furry. Erin is quiet. Erin is red. Harry is quiet. Harry is red. Harry is round. Round things are quiet.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Round things are quiet.
((("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
Anne is furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "+")
triple1
Harry is not red.
False
1
inv-proof
[(triple14)]
("Harry" "is" "red" "-")
triple14
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Anne is furry.[(triple1)] Anne is kind.[(triple2)] Anne is quiet.[(triple3)] Anne is red.[(triple4)] Charlie is big.[(triple5)] Charlie is kind.[(triple6)] Charlie is quiet.[(triple7 OR ((triple9) -> rule1))] Charlie is red.[(triple8)] Charlie is round.[(triple9)] Erin is furry.[(triple10)] Erin is quiet.[(triple11)] Erin is red.[(triple12)] Harry is quiet.[(triple13 OR ((triple15) -> rule1))] Harry is red.[(triple14)] Harry is round.[(triple15)]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
Charlie is big.
("Charlie" "is" "big" "+")
triple5
Charlie is kind.
("Charlie" "is" "kind" "+")
triple6
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple7
((triple9) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple8
Charlie is round.
("Charlie" "is" "round" "+")
triple9
Erin is furry.
("Erin" "is" "furry" "+")
triple10
Erin is quiet.
("Erin" "is" "quiet" "+")
triple11
Erin is red.
("Erin" "is" "red" "+")
triple12
Harry is quiet.
("Harry" "is" "quiet" "+")
triple13
((triple15) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple14
Harry is round.
("Harry" "is" "round" "+")
triple15