Dave is green. Erin is young. If Dave is cold then Dave is green. If someone is young then they are smart. If someone is young and cold then they are kind. If Dave is smart then Dave is cold. If Dave is green then Dave is smart. If Erin is smart and Erin is cold then Erin is big. If Dave is cold then Dave is big. If Erin is big and Erin is kind then Erin is young.
Dave is green.
("Dave" "is" "green" "+")
Erin is young.
("Erin" "is" "young" "+")
If Dave is cold then Dave is green.
((("Dave" "is" "cold" "+")) -> ("Dave" "is" "green" "+"))
If someone is young then they are smart.
((("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
If someone is young and cold then they are kind.
((("someone" "is" "young" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
If Dave is smart then Dave is cold.
((("Dave" "is" "smart" "+")) -> ("Dave" "is" "cold" "+"))
If Dave is green then Dave is smart.
((("Dave" "is" "green" "+")) -> ("Dave" "is" "smart" "+"))
If Erin is smart and Erin is cold then Erin is big.
((("Erin" "is" "smart" "+") ("Erin" "is" "cold" "+")) -> ("Erin" "is" "big" "+"))
If Dave is cold then Dave is big.
((("Dave" "is" "cold" "+")) -> ("Dave" "is" "big" "+"))
If Erin is big and Erin is kind then Erin is young.
((("Erin" "is" "big" "+") ("Erin" "is" "kind" "+")) -> ("Erin" "is" "young" "+"))
Dave is green.
True
1
proof
[(triple1)]
("Dave" "is" "green" "+")
triple1
Erin is not young.
False
1
inv-proof
[(triple2)]
("Erin" "is" "young" "-")
triple2
Erin is smart.
True
2
proof
[(((triple2) -> rule2))]
("Erin" "is" "smart" "+")
((triple2) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is not smart.
False
2
inv-proof
[(((triple2) -> rule2))]
("Erin" "is" "smart" "-")
((triple2) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Dave is cold.
True
3
proof
[(((((triple1) -> rule5)) -> rule4))]
("Dave" "is" "cold" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not cold.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule4))]
("Dave" "is" "cold" "-")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is big.
True
4
proof
[(((((((triple1) -> rule5)) -> rule4)) -> rule7))]
("Dave" "is" "big" "+")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is not big.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule4)) -> rule7))]
("Dave" "is" "big" "-")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is not kind.
Unknown
inv-rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "kind" "-")
Erin is kind.
Unknown
rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "kind" "+")
Erin is not big.
Unknown
inv-rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "big" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
@0: Dave is green.[(triple1)] Erin is young.[(triple2)] @1: Dave is smart.[(((triple1) -> rule5))] Erin is smart.[(((triple2) -> rule2))] @2: Dave is cold.[(((((triple1) -> rule5)) -> rule4))] @3: Dave is big.[(((((((triple1) -> rule5)) -> rule4)) -> rule7))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Erin is young.
("Erin" "is" "young" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
((triple1) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple2) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3