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