Charlie is big. Charlie is quiet. Harry is big. Harry is not blue. Harry is not red. Harry is round. Harry is smart. Blue things are not round. Big, smart things are round. Nice things are round. If Charlie is nice and Charlie is blue then Charlie is smart. All big, quiet things are blue. If Charlie is blue then Charlie is big.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is not blue.
("Harry" "is" "blue" "-")
Harry is not red.
("Harry" "is" "red" "-")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Blue things are not round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "-"))
Big, smart things are round.
((("something" "is" "big" "+") ("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
Nice things are round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
If Charlie is nice and Charlie is blue then Charlie is smart.
((("Charlie" "is" "nice" "+") ("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "smart" "+"))
All big, quiet things are blue.
((("something" "is" "big" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
If Charlie is blue then Charlie is big.
((("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "big" "+"))
Harry is smart.
True
1
proof
[(triple7)]
("Harry" "is" "smart" "+")
triple7
Harry is red.
False
1
inv-proof
[(triple5)]
("Harry" "is" "red" "+")
triple5
Charlie is blue.
True
3
proof
[(((triple1 triple2) -> rule5))]
("Charlie" "is" "blue" "+")
((triple1 triple2) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is not blue.
False
3
inv-proof
[(((triple1 triple2) -> rule5))]
("Charlie" "is" "blue" "-")
((triple1 triple2) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is not round.
True
4
proof
[(((((triple1 triple2) -> rule5)) -> rule1))]
("Charlie" "is" "round" "-")
((((triple1 triple2) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is round.
False
4
inv-proof
[(((((triple1 triple2) -> rule5)) -> rule1))]
("Charlie" "is" "round" "+")
((((triple1 triple2) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "smart" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Charlie is big.[(triple1)] Charlie is quiet.[(triple2)] Harry is big.[(triple3)] Harry is not blue.[(triple4)] Harry is not red.[(triple5)] Harry is round.[(triple6 OR ((triple3 triple7) -> rule2))] Harry is smart.[(triple7)] @1: Charlie is blue.[(((triple1 triple2) -> rule5))] @2: Charlie is not round.[(((((triple1 triple2) -> rule5)) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Harry is big.
("Harry" "is" "big" "+")
triple3
Harry is not blue.
("Harry" "is" "blue" "-")
triple4
Harry is not red.
("Harry" "is" "red" "-")
triple5
Harry is round.
("Harry" "is" "round" "+")
triple6
((triple3 triple7) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple1 triple2) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is not round.
("Charlie" "is" "round" "-")
((((triple1 triple2) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2