Anne is big. Anne is green. Dave is not big. Dave is green. Dave is round. Dave is smart. Erin is big. Erin is not green. Erin is rough. Erin is round. Erin is smart. Harry is not big. Harry is green. Harry is rough. Harry is not young. If something is young and big then it is round. If something is blue and not young then it is big. All blue things are not smart. If something is blue and not young then it is green. If something is rough and not young then it is green. If Dave is not big then Dave is green.
Anne is big.
("Anne" "is" "big" "+")
Anne is green.
("Anne" "is" "green" "+")
Dave is not big.
("Dave" "is" "big" "-")
Dave is green.
("Dave" "is" "green" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is not green.
("Erin" "is" "green" "-")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Harry is not big.
("Harry" "is" "big" "-")
Harry is green.
("Harry" "is" "green" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is not young.
("Harry" "is" "young" "-")
If something is young and big then it is round.
((("something" "is" "young" "+") ("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If something is blue and not young then it is big.
((("something" "is" "blue" "+") ("something" "is" "young" "~")) -> ("something" "is" "big" "+"))
All blue things are not smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "-"))
If something is blue and not young then it is green.
((("something" "is" "blue" "+") ("something" "is" "young" "~")) -> ("something" "is" "green" "+"))
If something is rough and not young then it is green.
((("something" "is" "rough" "+") ("something" "is" "young" "~")) -> ("something" "is" "green" "+"))
If Dave is not big then Dave is green.
((("Dave" "is" "big" "~")) -> ("Dave" "is" "green" "+"))
Erin is round.
True
1
proof
[(triple10)]
("Erin" "is" "round" "+")
triple10
Anne is not green.
False
1
inv-proof
[(triple2)]
("Anne" "is" "green" "-")
triple2
Anne is not round.
Unknown
inv-rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "round" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Anne is big.[(triple1)] Anne is green.[(triple2)] Dave is green.[(triple4 OR ((triple3) -> rule6))] Dave is not big.[(triple3)] Dave is round.[(triple5)] Dave is smart.[(triple6)] Erin is big.[(triple7)] Erin is not green.[(triple8)] Erin is rough.[(triple9)] Erin is round.[(triple10)] Erin is smart.[(triple11)] Harry is green.[(triple13 OR ((triple14 triple15) -> rule5))] Harry is not big.[(triple12)] Harry is not young.[(triple15)] Harry is rough.[(triple14)]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
triple4
((triple3) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not big.
("Dave" "is" "big" "-")
triple3
Dave is round.
("Dave" "is" "round" "+")
triple5
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Erin is big.
("Erin" "is" "big" "+")
triple7
Erin is not green.
("Erin" "is" "green" "-")
triple8
Erin is rough.
("Erin" "is" "rough" "+")
triple9
Erin is round.
("Erin" "is" "round" "+")
triple10
Erin is smart.
("Erin" "is" "smart" "+")
triple11
Harry is green.
("Harry" "is" "green" "+")
triple13
((triple14 triple15) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not big.
("Harry" "is" "big" "-")
triple12
Harry is not young.
("Harry" "is" "young" "-")
triple15
Harry is rough.
("Harry" "is" "rough" "+")
triple14