Charlie is furry. Charlie is green. Charlie is not quiet. Charlie is rough. Erin is blue. Erin is not green. Erin is rough. Harry is big. Harry is blue. Harry is quiet. Harry is rough. Harry is round. If something is blue then it is big. If something is furry then it is big. All blue things are big. All green things are rough. If something is blue and not rough then it is quiet. If Charlie is round and Charlie is quiet then Charlie is big. All green, quiet things are round. All furry things are round.
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
Charlie is rough.
("Charlie" "is" "rough" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is not green.
("Erin" "is" "green" "-")
Erin is rough.
("Erin" "is" "rough" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
If something is blue then it is big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If something is furry then it is big.
((("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
All blue things are big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
All green things are rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
If something is blue and not rough then it is quiet.
((("something" "is" "blue" "+") ("something" "is" "rough" "~")) -> ("something" "is" "quiet" "+"))
If Charlie is round and Charlie is quiet then Charlie is big.
((("Charlie" "is" "round" "+") ("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "big" "+"))
All green, quiet things are round.
((("something" "is" "green" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
All furry things are round.
((("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
Erin is blue.
True
1
proof
[(triple5)]
("Erin" "is" "blue" "+")
triple5
Harry is not big.
False
1
inv-proof
[(triple8 OR ((triple9) -> rule1) OR ((triple9) -> rule3))]
("Harry" "is" "big" "-")
triple8
((triple9) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple9) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Charlie is big.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "big" "+")
((triple1) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not big.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "big" "-")
((triple1) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Erin is not round.
Unknown
inv-rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "round" "-")
Erin is quiet.
Unknown
rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "quiet" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
@0: Charlie is furry.[(triple1)] Charlie is green.[(triple2)] Charlie is not quiet.[(triple3)] Charlie is rough.[(triple4 OR ((triple2) -> rule4))] Erin is blue.[(triple5)] Erin is not green.[(triple6)] Erin is rough.[(triple7)] Harry is big.[(triple8 OR ((triple9) -> rule1) OR ((triple9) -> rule3))] Harry is blue.[(triple9)] Harry is quiet.[(triple10)] Harry is rough.[(triple11)] Harry is round.[(triple12)] @1: Charlie is big.[(((triple1) -> rule2))] Charlie is round.[(((triple1) -> rule8))] Erin is big.[(((triple5) -> rule1) OR ((triple5) -> rule3))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
((triple2) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple5
Erin is not green.
("Erin" "is" "green" "-")
triple6
Erin is rough.
("Erin" "is" "rough" "+")
triple7
Harry is big.
("Harry" "is" "big" "+")
triple8
((triple9) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple9) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
Harry is rough.
("Harry" "is" "rough" "+")
triple11
Harry is round.
("Harry" "is" "round" "+")
triple12
Charlie is big.
("Charlie" "is" "big" "+")
((triple1) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple1) -> (rule8 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple5) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple5) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1