Bob is quiet. Bob is smart. Gary is blue. Gary is smart. Harry is blue. Harry is not cold. Harry is smart. Quiet people are young. If someone is young then they are round.
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is not cold.
("Harry" "is" "cold" "-")
Harry is smart.
("Harry" "is" "smart" "+")
Quiet people are young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
If someone is young then they are round.
((("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
Bob is smart.
True
1
proof
[(triple2)]
("Bob" "is" "smart" "+")
triple2
Harry is not smart.
False
1
inv-proof
[(triple7)]
("Harry" "is" "smart" "-")
triple7
Bob is young.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "young" "+")
((triple1) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not young.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "young" "-")
((triple1) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is round.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("Bob" "is" "round" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is not round.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("Bob" "is" "round" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Gary is not round.
Unknown
inv-rconc
[@2: Gary is round.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Gary" "is" "round" "-")
Gary is young.
Unknown
rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "young" "+")
Harry is not round.
Unknown
inv-rconc
[@2: Harry is round.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Harry" "is" "round" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is quiet.[(triple1)] Bob is smart.[(triple2)] Gary is blue.[(triple3)] Gary is smart.[(triple4)] Harry is blue.[(triple5)] Harry is not cold.[(triple6)] Harry is smart.[(triple7)] @1: Bob is young.[(((triple1) -> rule1))] @2: Bob is round.[(((((triple1) -> rule1)) -> rule2))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Gary is blue.
("Gary" "is" "blue" "+")
triple3
Gary is smart.
("Gary" "is" "smart" "+")
triple4
Harry is blue.
("Harry" "is" "blue" "+")
triple5
Harry is not cold.
("Harry" "is" "cold" "-")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Bob is young.
("Bob" "is" "young" "+")
((triple1) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2