Bob is big. Bob is not smart. Bob is white. Dave is furry. Dave is quiet. Erin is not furry. Erin is not quiet. Erin is red. Erin is not white. Erin is young. All young, big things are furry. White things are red. Furry, white things are red. All furry, big things are red. If something is smart then it is white. All furry, quiet things are smart.
Bob is big.
("Bob" "is" "big" "+")
Bob is not smart.
("Bob" "is" "smart" "-")
Bob is white.
("Bob" "is" "white" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is not furry.
("Erin" "is" "furry" "-")
Erin is not quiet.
("Erin" "is" "quiet" "-")
Erin is red.
("Erin" "is" "red" "+")
Erin is not white.
("Erin" "is" "white" "-")
Erin is young.
("Erin" "is" "young" "+")
All young, big things are furry.
((("something" "is" "young" "+") ("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
White things are red.
((("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
Furry, white things are red.
((("something" "is" "furry" "+") ("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
All furry, big things are red.
((("something" "is" "furry" "+") ("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If something is smart then it is white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
All furry, quiet things are smart.
((("something" "is" "furry" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
Bob is not smart.
True
1
proof
[(triple2)]
("Bob" "is" "smart" "-")
triple2
Erin is not young.
False
1
inv-proof
[(triple10)]
("Erin" "is" "young" "-")
triple10
Bob is red.
True
2
proof
[(((triple3) -> rule2))]
("Bob" "is" "red" "+")
((triple3) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Dave is not smart.
False
3
inv-proof
[(((triple4 triple5) -> rule6))]
("Dave" "is" "smart" "-")
((triple4 triple5) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is white.
True
4
proof
[(((((triple4 triple5) -> rule6)) -> rule5))]
("Dave" "is" "white" "+")
((((triple4 triple5) -> (rule6 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not white.
False
4
inv-proof
[(((((triple4 triple5) -> rule6)) -> rule5))]
("Dave" "is" "white" "-")
((((triple4 triple5) -> (rule6 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is red.
True
5
proof
[(((((((triple4 triple5) -> rule6)) -> rule5)) -> rule2) OR ((triple4 ((((triple4 triple5) -> rule6)) -> rule5)) -> rule3))]
("Dave" "is" "red" "+")
((((((triple4 triple5) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
((triple4 ((((triple4 triple5) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is not red.
False
5
inv-proof
[(((((((triple4 triple5) -> rule6)) -> rule5)) -> rule2) OR ((triple4 ((((triple4 triple5) -> rule6)) -> rule5)) -> rule3))]
("Dave" "is" "red" "-")
((((((triple4 triple5) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
((triple4 ((((triple4 triple5) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Bob is not furry.
Unknown
inv-rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "furry" "-")
Erin is smart.
Unknown
rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "smart" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Erin is not big.
Unknown
inv-random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Bob is big.[(triple1)] Bob is not smart.[(triple2)] Bob is white.[(triple3)] Dave is furry.[(triple4)] Dave is quiet.[(triple5)] Erin is not furry.[(triple6)] Erin is not quiet.[(triple7)] Erin is not white.[(triple9)] Erin is red.[(triple8)] Erin is young.[(triple10)] @1: Bob is red.[(((triple3) -> rule2))] Dave is smart.[(((triple4 triple5) -> rule6))] @2: Dave is white.[(((((triple4 triple5) -> rule6)) -> rule5))] @3: Dave is red.[(((((((triple4 triple5) -> rule6)) -> rule5)) -> rule2) OR ((triple4 ((((triple4 triple5) -> rule6)) -> rule5)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is not smart.
("Bob" "is" "smart" "-")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
Erin is not furry.
("Erin" "is" "furry" "-")
triple6
Erin is not quiet.
("Erin" "is" "quiet" "-")
triple7
Erin is not white.
("Erin" "is" "white" "-")
triple9
Erin is red.
("Erin" "is" "red" "+")
triple8
Erin is young.
("Erin" "is" "young" "+")
triple10
Bob is red.
("Bob" "is" "red" "+")
((triple3) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple4 triple5) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((((triple4 triple5) -> (rule6 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((((((triple4 triple5) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
((triple4 ((((triple4 triple5) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3