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