Bob is quiet. Bob is round. Dave is young. Gary is furry. Gary is quiet. Gary is not round. Gary is smart. If Dave is quiet and Dave is smart then Dave is young. If something is smart and cold then it is nice. If Bob is cold and Bob is smart then Bob is quiet. If something is smart and nice then it is round. Young things are smart. Smart, young things are cold.
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is not round.
("Gary" "is" "round" "-")
Gary is smart.
("Gary" "is" "smart" "+")
If Dave is quiet and Dave is smart then Dave is young.
((("Dave" "is" "quiet" "+") ("Dave" "is" "smart" "+")) -> ("Dave" "is" "young" "+"))
If something is smart and cold then it is nice.
((("something" "is" "smart" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If Bob is cold and Bob is smart then Bob is quiet.
((("Bob" "is" "cold" "+") ("Bob" "is" "smart" "+")) -> ("Bob" "is" "quiet" "+"))
If something is smart and nice then it is round.
((("something" "is" "smart" "+") ("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
Young things are smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
Smart, young things are cold.
((("something" "is" "smart" "+") ("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
Gary is quiet.
True
1
proof
[(triple5)]
("Gary" "is" "quiet" "+")
triple5
Gary is not furry.
False
1
inv-proof
[(triple4)]
("Gary" "is" "furry" "-")
triple4
Dave is smart.
True
2
proof
[(((triple3) -> rule5))]
("Dave" "is" "smart" "+")
((triple3) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not smart.
False
2
inv-proof
[(((triple3) -> rule5))]
("Dave" "is" "smart" "-")
((triple3) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is cold.
True
4
proof
[(((((triple3) -> rule5) triple3) -> rule6))]
("Dave" "is" "cold" "+")
((((triple3) -> (rule5 % int2)) triple3) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not cold.
False
4
inv-proof
[(((((triple3) -> rule5) triple3) -> rule6))]
("Dave" "is" "cold" "-")
((((triple3) -> (rule5 % int2)) triple3) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is nice.
True
7
proof
[(((((triple3) -> rule5) ((((triple3) -> rule5) triple3) -> rule6)) -> rule2))]
("Dave" "is" "nice" "+")
((((triple3) -> (rule5 % int3)) ((((triple3) -> (rule5 % int3)) triple3) -> (rule6 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is not nice.
False
7
inv-proof
[(((((triple3) -> rule5) ((((triple3) -> rule5) triple3) -> rule6)) -> rule2))]
("Dave" "is" "nice" "-")
((((triple3) -> (rule5 % int3)) ((((triple3) -> (rule5 % int3)) triple3) -> (rule6 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Gary is not cold.
Unknown
inv-rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "cold" "-")
Bob is smart.
Unknown
rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "smart" "+")
Bob is not nice.
Unknown
inv-rconc
[@2: Bob is nice.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Bob" "is" "nice" "-")
Bob is cold.
Unknown
rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "cold" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Bob is quiet.[(triple1)] Bob is round.[(triple2)] Dave is young.[(triple3)] Gary is furry.[(triple4)] Gary is not round.[(triple6)] Gary is quiet.[(triple5)] Gary is smart.[(triple7)] @1: Dave is smart.[(((triple3) -> rule5))] @2: Dave is cold.[(((((triple3) -> rule5) triple3) -> rule6))] @3: Dave is nice.[(((((triple3) -> rule5) ((((triple3) -> rule5) triple3) -> rule6)) -> rule2))] @4: Dave is round.[(((((triple3) -> rule5) ((((triple3) -> rule5) ((((triple3) -> rule5) triple3) -> rule6)) -> rule2)) -> rule4))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Dave is young.
("Dave" "is" "young" "+")
triple3
Gary is furry.
("Gary" "is" "furry" "+")
triple4
Gary is not round.
("Gary" "is" "round" "-")
triple6
Gary is quiet.
("Gary" "is" "quiet" "+")
triple5
Gary is smart.
("Gary" "is" "smart" "+")
triple7
Dave is smart.
("Dave" "is" "smart" "+")
((triple3) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((((triple3) -> (rule5 % int2)) triple3) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((((triple3) -> (rule5 % int3)) ((((triple3) -> (rule5 % int3)) triple3) -> (rule6 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
((((triple3) -> (rule5 % int4)) ((((triple3) -> (rule5 % int4)) ((((triple3) -> (rule5 % int4)) triple3) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4