Charlie is green. Charlie is nice. Charlie is smart. Erin is big. Erin is furry. Erin is green. Erin is nice. Erin is red. Erin is round. Erin is smart. Gary is big. Gary is furry. Gary is green. Gary is smart. Harry is smart. If something is red then it is nice. Smart, nice things are round. If something is big and green then it is red.
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If something is red then it is nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
Smart, nice things are round.
((("something" "is" "smart" "+") ("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
If something is big and green then it is red.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
Erin is nice.
True
1
proof
[(triple7 OR ((triple8) -> rule1) OR ((((triple4 triple6) -> rule3)) -> rule1))]
("Erin" "is" "nice" "+")
triple7
((triple8) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((triple4 triple6) -> (rule3 % int2))) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Gary is not smart.
False
1
inv-proof
[(triple14)]
("Gary" "is" "smart" "-")
triple14
Gary is red.
True
3
proof
[(((triple11 triple13) -> rule3))]
("Gary" "is" "red" "+")
((triple11 triple13) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Charlie is not round.
False
3
inv-proof
[(((triple3 triple2) -> rule2))]
("Charlie" "is" "round" "-")
((triple3 triple2) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Gary is nice.
True
4
proof
[(((((triple11 triple13) -> rule3)) -> rule1))]
("Gary" "is" "nice" "+")
((((triple11 triple13) -> (rule3 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not nice.
False
4
inv-proof
[(((((triple11 triple13) -> rule3)) -> rule1))]
("Gary" "is" "nice" "-")
((((triple11 triple13) -> (rule3 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is round.
True
6
proof
[(((triple14 ((((triple11 triple13) -> rule3)) -> rule1)) -> rule2))]
("Gary" "is" "round" "+")
((triple14 ((((triple11 triple13) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is not round.
False
6
inv-proof
[(((triple14 ((((triple11 triple13) -> rule3)) -> rule1)) -> rule2))]
("Gary" "is" "round" "-")
((triple14 ((((triple11 triple13) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Charlie is not red.
Unknown
inv-rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "red" "-")
Harry is nice.
Unknown
rconc
[@2: Harry is nice.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Harry" "is" "nice" "+")
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "red" "-")
Harry is round.
Unknown
rconc
[@3: Harry is round.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule3 <- FAIL)]]
("Harry" "is" "round" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Charlie is green.[(triple1)] Charlie is nice.[(triple2)] Charlie is smart.[(triple3)] Erin is big.[(triple4)] Erin is furry.[(triple5)] Erin is green.[(triple6)] Erin is nice.[(triple7 OR ((triple8) -> rule1) OR ((((triple4 triple6) -> rule3)) -> rule1))] Erin is red.[(triple8 OR ((triple4 triple6) -> rule3))] Erin is round.[(triple9 OR ((triple10 triple7) -> rule2) OR ((triple10 ((triple8) -> rule1)) -> rule2) OR ((triple10 ((((triple4 triple6) -> rule3)) -> rule1)) -> rule2))] Erin is smart.[(triple10)] Gary is big.[(triple11)] Gary is furry.[(triple12)] Gary is green.[(triple13)] Gary is smart.[(triple14)] Harry is smart.[(triple15)] @1: Charlie is round.[(((triple3 triple2) -> rule2))] Gary is red.[(((triple11 triple13) -> rule3))] @2: Gary is nice.[(((((triple11 triple13) -> rule3)) -> rule1))] @3: Gary is round.[(((triple14 ((((triple11 triple13) -> rule3)) -> rule1)) -> rule2))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
triple4
Erin is furry.
("Erin" "is" "furry" "+")
triple5
Erin is green.
("Erin" "is" "green" "+")
triple6
Erin is nice.
("Erin" "is" "nice" "+")
triple7
((triple8) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((triple4 triple6) -> (rule3 % int2))) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
triple8
((triple4 triple6) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple9
((triple10 triple7) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple10 ((triple8) -> (rule1 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((triple10 ((((triple4 triple6) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
triple10
Gary is big.
("Gary" "is" "big" "+")
triple11
Gary is furry.
("Gary" "is" "furry" "+")
triple12
Gary is green.
("Gary" "is" "green" "+")
triple13
Gary is smart.
("Gary" "is" "smart" "+")
triple14
Harry is smart.
("Harry" "is" "smart" "+")
triple15
Charlie is round.
("Charlie" "is" "round" "+")
((triple3 triple2) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple11 triple13) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((((triple11 triple13) -> (rule3 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((triple14 ((((triple11 triple13) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3