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