Bob is smart. Charlie is red. Gary is red. Harry is big. All nice things are red. If Harry is red and Harry is young then Harry is kind. Smart things are big. Nice things are round. If something is red then it is big. All big, red things are smart. All smart, nice things are young. If something is young then it is smart.
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Gary is red.
("Gary" "is" "red" "+")
Harry is big.
("Harry" "is" "big" "+")
All nice things are red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If Harry is red and Harry is young then Harry is kind.
((("Harry" "is" "red" "+") ("Harry" "is" "young" "+")) -> ("Harry" "is" "kind" "+"))
Smart things are big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
Nice things are round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
If something is red then it is big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
All big, red things are smart.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
All smart, nice things are young.
((("something" "is" "smart" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
If something is young then it is smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
Charlie is red.
True
1
proof
[(triple2)]
("Charlie" "is" "red" "+")
triple2
Harry is not big.
False
1
inv-proof
[(triple4)]
("Harry" "is" "big" "-")
triple4
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "red" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is smart.[(triple1)] Charlie is red.[(triple2)] Gary is red.[(triple3)] Harry is big.[(triple4)] @1: Bob is big.[(((triple1) -> rule3))] Charlie is big.[(((triple2) -> rule5))] Gary is big.[(((triple3) -> rule5))] @2: Charlie is smart.[(((((triple2) -> rule5) triple2) -> rule6))] Gary is smart.[(((((triple3) -> rule5) triple3) -> rule6))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Gary is red.
("Gary" "is" "red" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
triple4
Bob is big.
("Bob" "is" "big" "+")
((triple1) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((triple2) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple3) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple2) -> (rule5 % int2)) triple2) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((((triple3) -> (rule5 % int2)) triple3) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2