Charlie is big. Charlie is green. Charlie is red. Charlie is smart. Fiona is round. Gary is not furry. Gary is red. Gary is round. Gary is not smart. Harry is green. Harry is not round. Harry is smart. All smart people are big. All kind people are red. If someone is big and not furry then they are red. Smart, red people are green. Big, green people are kind. If someone is red and not kind then they are round. If someone is furry and red then they are not round. Big, kind people are not round.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Gary is not furry.
("Gary" "is" "furry" "-")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is not smart.
("Gary" "is" "smart" "-")
Harry is green.
("Harry" "is" "green" "+")
Harry is not round.
("Harry" "is" "round" "-")
Harry is smart.
("Harry" "is" "smart" "+")
All smart people are big.
((("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
All kind people are red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
If someone is big and not furry then they are red.
((("someone" "is" "big" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "red" "+"))
Smart, red people are green.
((("someone" "is" "smart" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
Big, green people are kind.
((("someone" "is" "big" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
If someone is red and not kind then they are round.
((("someone" "is" "red" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "round" "+"))
If someone is furry and red then they are not round.
((("someone" "is" "furry" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "round" "-"))
Big, kind people are not round.
((("someone" "is" "big" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "round" "-"))
Harry is green.
True
1
proof
[(triple10)]
("Harry" "is" "green" "+")
triple10
Charlie is not red.
False
1
inv-proof
[(triple3 OR ((((triple1 triple2) -> rule5)) -> rule2) OR ((((((triple4) -> rule1) triple2) -> rule5)) -> rule2))]
("Charlie" "is" "red" "-")
triple3
((((triple1 triple2) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((((triple4) -> (rule1 % int3)) triple2) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Harry is big.
True
2
proof
[(((triple12) -> rule1))]
("Harry" "is" "big" "+")
((triple12) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Charlie is not kind.
False
3
inv-proof
[(((triple1 triple2) -> rule5) OR ((triple1 ((triple4 triple3) -> rule4)) -> rule5) OR ((((triple4) -> rule1) triple2) -> rule5) OR ((((triple4) -> rule1) ((triple4 triple3) -> rule4)) -> rule5))]
("Charlie" "is" "kind" "-")
((triple1 triple2) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple1 ((triple4 triple3) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((triple4) -> (rule1 % int2)) triple2) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple4) -> (rule1 % int3)) ((triple4 triple3) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Harry is kind.
True
4
proof
[(((((triple12) -> rule1) triple10) -> rule5))]
("Harry" "is" "kind" "+")
((((triple12) -> (rule1 % int2)) triple10) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not kind.
False
4
inv-proof
[(((((triple12) -> rule1) triple10) -> rule5))]
("Harry" "is" "kind" "-")
((((triple12) -> (rule1 % int2)) triple10) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is red.
True
5
proof
[(((((((triple12) -> rule1) triple10) -> rule5)) -> rule2))]
("Harry" "is" "red" "+")
((((((triple12) -> (rule1 % int3)) triple10) -> (rule5 % int2))) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is not red.
False
5
inv-proof
[(((((((triple12) -> rule1) triple10) -> rule5)) -> rule2))]
("Harry" "is" "red" "-")
((((((triple12) -> (rule1 % int3)) triple10) -> (rule5 % int2))) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Fiona is not red.
Unknown
inv-rconc
[@3: Fiona is red.[CWA. Example of deepest failure = (rule2 <- rule5 <- rule1 <- FAIL)]]
("Fiona" "is" "red" "-")
Gary is kind.
Unknown
rconc
[@2: Gary is kind.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Gary" "is" "kind" "+")
Gary is not green.
Unknown
inv-rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "green" "-")
Gary is big.
Unknown
rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "big" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Fiona is furry.
Unknown
random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "+")
@0: Charlie is big.[(triple1 OR ((triple4) -> rule1))] Charlie is green.[(triple2 OR ((triple4 triple3) -> rule4))] Charlie is red.[(triple3 OR ((((triple1 triple2) -> rule5)) -> rule2) OR ((((((triple4) -> rule1) triple2) -> rule5)) -> rule2))] Charlie is smart.[(triple4)] Fiona is round.[(triple5)] Gary is not furry.[(triple6)] Gary is not smart.[(triple9)] Gary is red.[(triple7)] Gary is round.[(triple8)] Harry is green.[(triple10)] Harry is not round.[(triple11 OR ((((triple12) -> rule1) ((((triple12) -> rule1) triple10) -> rule5)) -> rule8))] Harry is smart.[(triple12)] @1: Charlie is kind.[(((triple1 triple2) -> rule5) OR ((triple1 ((triple4 triple3) -> rule4)) -> rule5) OR ((((triple4) -> rule1) triple2) -> rule5) OR ((((triple4) -> rule1) ((triple4 triple3) -> rule4)) -> rule5))] Harry is big.[(((triple12) -> rule1))] @2: Charlie is not round.[(((triple1 ((triple1 triple2) -> rule5)) -> rule8) OR ((((triple4) -> rule1) ((triple1 triple2) -> rule5)) -> rule8) OR ((triple1 ((triple1 ((triple4 triple3) -> rule4)) -> rule5)) -> rule8) OR ((triple1 ((((triple4) -> rule1) triple2) -> rule5)) -> rule8) OR ((triple1 ((((triple4) -> rule1) ((triple4 triple3) -> rule4)) -> rule5)) -> rule8) OR ((((triple4) -> rule1) ((triple1 ((triple4 triple3) -> rule4)) -> rule5)) -> rule8) OR ((((triple4) -> rule1) ((((triple4) -> rule1) triple2) -> rule5)) -> rule8) OR ((((triple4) -> rule1) ((((triple4) -> rule1) ((triple4 triple3) -> rule4)) -> rule5)) -> rule8))] Harry is kind.[(((((triple12) -> rule1) triple10) -> rule5))] @3: Harry is red.[(((((((triple12) -> rule1) triple10) -> rule5)) -> rule2))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple4) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
((triple4 triple3) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple3
((((triple1 triple2) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((((triple4) -> (rule1 % int3)) triple2) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
Fiona is round.
("Fiona" "is" "round" "+")
triple5
Gary is not furry.
("Gary" "is" "furry" "-")
triple6
Gary is not smart.
("Gary" "is" "smart" "-")
triple9
Gary is red.
("Gary" "is" "red" "+")
triple7
Gary is round.
("Gary" "is" "round" "+")
triple8
Harry is green.
("Harry" "is" "green" "+")
triple10
Harry is not round.
("Harry" "is" "round" "-")
triple11
((((triple12) -> (rule1 % int3)) ((((triple12) -> (rule1 % int3)) triple10) -> (rule5 % int2))) -> (rule8 % int1))
Harry is not round.
("Harry" "is" "round" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple1 triple2) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple1 ((triple4 triple3) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((triple4) -> (rule1 % int2)) triple2) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple4) -> (rule1 % int3)) ((triple4 triple3) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
((triple12) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Charlie is not round.
("Charlie" "is" "round" "-")
((triple1 ((triple1 triple2) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple4) -> (rule1 % int3)) ((triple1 triple2) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((triple1 ((triple1 ((triple4 triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
((triple1 ((((triple4) -> (rule1 % int3)) triple2) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((triple1 ((((triple4) -> (rule1 % int4)) ((triple4 triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
((((triple4) -> (rule1 % int4)) ((triple1 ((triple4 triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
((((triple4) -> (rule1 % int3)) ((((triple4) -> (rule1 % int3)) triple2) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((triple4) -> (rule1 % int4)) ((((triple4) -> (rule1 % int4)) ((triple4 triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Harry is kind.
("Harry" "is" "kind" "+")
((((triple12) -> (rule1 % int2)) triple10) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((((((triple12) -> (rule1 % int3)) triple10) -> (rule5 % int2))) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3