Bob is not young. Dave is nice. All young things are blue. All cold things are blue. If something is blue then it is cold. If something is nice then it is young. If Bob is quiet then Bob is nice. If Dave is young then Dave is smart. If Dave is nice then Dave is young. If Bob is round and Bob is young then Bob is quiet.
Bob is not young.
("Bob" "is" "young" "-")
Dave is nice.
("Dave" "is" "nice" "+")
All young things are blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
All cold things are blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
If something is blue then it is cold.
((("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
If something is nice then it is young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
If Bob is quiet then Bob is nice.
((("Bob" "is" "quiet" "+")) -> ("Bob" "is" "nice" "+"))
If Dave is young then Dave is smart.
((("Dave" "is" "young" "+")) -> ("Dave" "is" "smart" "+"))
If Dave is nice then Dave is young.
((("Dave" "is" "nice" "+")) -> ("Dave" "is" "young" "+"))
If Bob is round and Bob is young then Bob is quiet.
((("Bob" "is" "round" "+") ("Bob" "is" "young" "+")) -> ("Bob" "is" "quiet" "+"))
Dave is nice.
True
1
proof
[(triple2)]
("Dave" "is" "nice" "+")
triple2
Bob is young.
False
1
inv-proof
[(triple1)]
("Bob" "is" "young" "+")
triple1
Dave is young.
True
2
proof
[(((triple2) -> rule4) OR ((triple2) -> rule7))]
("Dave" "is" "young" "+")
((triple2) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple2) -> (rule7 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is not young.
False
2
inv-proof
[(((triple2) -> rule4) OR ((triple2) -> rule7))]
("Dave" "is" "young" "-")
((triple2) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple2) -> (rule7 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is blue.
True
3
proof
[(((((triple2) -> rule4)) -> rule1) OR ((((triple2) -> rule7)) -> rule1))]
("Dave" "is" "blue" "+")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((((triple2) -> (rule7 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is not smart.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule6) OR ((((triple2) -> rule7)) -> rule6))]
("Dave" "is" "smart" "-")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((((triple2) -> (rule7 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is cold.
True
4
proof
[(((((((triple2) -> rule4)) -> rule1)) -> rule3) OR ((((((triple2) -> rule7)) -> rule1)) -> rule3))]
("Dave" "is" "cold" "+")
((((((triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
((((((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not cold.
False
4
inv-proof
[(((((((triple2) -> rule4)) -> rule1)) -> rule3) OR ((((((triple2) -> rule7)) -> rule1)) -> rule3))]
("Dave" "is" "cold" "-")
((((((triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
((((((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Bob is not cold.
Unknown
inv-rconc
[@2: Bob is cold.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Bob" "is" "cold" "-")
Bob is nice.
Unknown
rconc
[@2: Bob is nice.[CWA. Example of deepest failure = (rule5 <- rule8 <- FAIL)]]
("Bob" "is" "nice" "+")
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "quiet" "-")
Bob is blue.
Unknown
rconc
[@3: Bob is blue.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule1 <- FAIL)]]
("Bob" "is" "blue" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Bob is not young.[(triple1)] Dave is nice.[(triple2)] @1: Dave is young.[(((triple2) -> rule4) OR ((triple2) -> rule7))] @2: Dave is blue.[(((((triple2) -> rule4)) -> rule1) OR ((((triple2) -> rule7)) -> rule1))] Dave is smart.[(((((triple2) -> rule4)) -> rule6) OR ((((triple2) -> rule7)) -> rule6))] @3: Dave is cold.[(((((((triple2) -> rule4)) -> rule1)) -> rule3) OR ((((((triple2) -> rule7)) -> rule1)) -> rule3))]
Bob is not young.
("Bob" "is" "young" "-")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
Dave is young.
("Dave" "is" "young" "+")
((triple2) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple2) -> (rule7 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((((triple2) -> (rule7 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((((triple2) -> (rule7 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((((((triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
((((((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3