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