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