Bob is smart. Harry is smart. All smart things are red. If something is kind and not quiet then it is red. All kind, quiet things are not nice. Smart, red things are nice. If something is smart and not quiet then it is nice. Furry, smart things are round.
Bob is smart.
("Bob" "is" "smart" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All smart things are red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
If something is kind and not quiet then it is red.
((("something" "is" "kind" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "red" "+"))
All kind, quiet things are not nice.
((("something" "is" "kind" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "nice" "-"))
Smart, red things are nice.
((("something" "is" "smart" "+") ("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
If something is smart and not quiet then it is nice.
((("something" "is" "smart" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "nice" "+"))
Furry, smart things are round.
((("something" "is" "furry" "+") ("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
Bob is smart.
True
1
proof
[(triple1)]
("Bob" "is" "smart" "+")
triple1
Harry is not smart.
False
1
inv-proof
[(triple2)]
("Harry" "is" "smart" "-")
triple2
Harry is red.
True
2
proof
[(((triple2) -> rule1))]
("Harry" "is" "red" "+")
((triple2) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Bob is not red.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "red" "-")
((triple1) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is nice.
True
4
proof
[(((triple1 ((triple1) -> rule1)) -> rule4))]
("Bob" "is" "nice" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is not nice.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule4))]
("Bob" "is" "nice" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "round" "-")
Harry is round.
Unknown
rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "round" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Bob is smart.[(triple1)] Harry is smart.[(triple2)] @1: Bob is red.[(((triple1) -> rule1))] Harry is red.[(((triple2) -> rule1))] @2: Bob is nice.[(((triple1 ((triple1) -> rule1)) -> rule4))] Harry is nice.[(((triple2 ((triple2) -> rule1)) -> rule4))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Harry is smart.
("Harry" "is" "smart" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
((triple1) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple2) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2