Anne is big. Anne is green. Anne is nice. Anne is quiet. Anne is young. Charlie is big. Charlie is furry. Charlie is green. Charlie is nice. Charlie is quiet. Charlie is smart. Charlie is young. Harry is big. Harry is quiet. Harry is smart. If someone is nice then they are green. All smart people are big. If Charlie is big then Charlie is quiet. If Harry is quiet then Harry is young. All furry people are green. All big, nice people are smart. If someone is big and young then they are smart. All furry, smart people are big.
Anne is big.
("Anne" "is" "big" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If someone is nice then they are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
All smart people are big.
((("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
If Charlie is big then Charlie is quiet.
((("Charlie" "is" "big" "+")) -> ("Charlie" "is" "quiet" "+"))
If Harry is quiet then Harry is young.
((("Harry" "is" "quiet" "+")) -> ("Harry" "is" "young" "+"))
All furry people are green.
((("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
All big, nice people are smart.
((("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
If someone is big and young then they are smart.
((("someone" "is" "big" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
All furry, smart people are big.
((("someone" "is" "furry" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
Charlie is furry.
True
1
proof
[(triple7)]
("Charlie" "is" "furry" "+")
triple7
Harry is not quiet.
False
1
inv-proof
[(triple14)]
("Harry" "is" "quiet" "-")
triple14
Anne is smart.
True
3
proof
[(((triple1 triple3) -> rule6) OR ((triple1 triple5) -> rule7))]
("Anne" "is" "smart" "+")
((triple1 triple3) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple1 triple5) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Harry is not young.
False
2
inv-proof
[(((triple14) -> rule4))]
("Harry" "is" "young" "-")
((triple14) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is not green.
Unknown
inv-rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "green" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is big.[(triple1)] Anne is green.[(triple2 OR ((triple3) -> rule1))] Anne is nice.[(triple3)] Anne is quiet.[(triple4)] Anne is young.[(triple5)] Charlie is big.[(triple6 OR ((triple11) -> rule2) OR ((triple7 triple11) -> rule8))] Charlie is furry.[(triple7)] Charlie is green.[(triple8 OR ((triple7) -> rule5) OR ((triple9) -> rule1))] Charlie is nice.[(triple9)] Charlie is quiet.[(triple10 OR ((triple6) -> rule3) OR ((((triple11) -> rule2)) -> rule3) OR ((((triple7 triple11) -> rule8)) -> rule3))] Charlie is smart.[(triple11 OR ((triple6 triple12) -> rule7) OR ((triple6 triple9) -> rule6))] Charlie is young.[(triple12)] Harry is big.[(triple13 OR ((triple15) -> rule2))] Harry is quiet.[(triple14)] Harry is smart.[(triple15 OR ((triple13 ((triple14) -> rule4)) -> rule7))] @1: Anne is smart.[(((triple1 triple3) -> rule6) OR ((triple1 triple5) -> rule7))] Harry is young.[(((triple14) -> rule4))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple3) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
triple5
Charlie is big.
("Charlie" "is" "big" "+")
triple6
((triple11) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple7 triple11) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple7
Charlie is green.
("Charlie" "is" "green" "+")
triple8
((triple7) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((triple9) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple9
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple10
((triple6) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((((triple11) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple7 triple11) -> (rule8 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple11
((triple6 triple12) -> (rule7 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple6 triple9) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
triple12
Harry is big.
("Harry" "is" "big" "+")
triple13
((triple15) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple14
Harry is smart.
("Harry" "is" "smart" "+")
triple15
((triple13 ((triple14) -> (rule4 % int2))) -> (rule7 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((triple1 triple3) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple1 triple5) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple14) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1