Bob is not big. Bob is cold. Bob is green. Bob is nice. Dave is big. Dave is smart. Fiona is not cold. If someone is quiet and nice then they are smart. If Fiona is cold and Fiona is smart then Fiona is young. All nice, big people are young. All young, green people are not cold. Smart people are green. All green, smart people are nice.
Bob is not big.
("Bob" "is" "big" "-")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is not cold.
("Fiona" "is" "cold" "-")
If someone is quiet and nice then they are smart.
((("someone" "is" "quiet" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
If Fiona is cold and Fiona is smart then Fiona is young.
((("Fiona" "is" "cold" "+") ("Fiona" "is" "smart" "+")) -> ("Fiona" "is" "young" "+"))
All nice, big people are young.
((("someone" "is" "nice" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
All young, green people are not cold.
((("someone" "is" "young" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "cold" "-"))
Smart people are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
All green, smart people are nice.
((("someone" "is" "green" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
Bob is nice.
True
1
proof
[(triple4)]
("Bob" "is" "nice" "+")
triple4
Bob is not green.
False
1
inv-proof
[(triple3)]
("Bob" "is" "green" "-")
triple3
Dave is green.
True
2
proof
[(((triple6) -> rule5))]
("Dave" "is" "green" "+")
((triple6) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple6) -> rule5))]
("Dave" "is" "green" "-")
((triple6) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
True
4
proof
[(((((triple6) -> rule5) triple6) -> rule6))]
("Dave" "is" "nice" "+")
((((triple6) -> (rule5 % int2)) triple6) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not nice.
False
4
inv-proof
[(((((triple6) -> rule5) triple6) -> rule6))]
("Dave" "is" "nice" "-")
((((triple6) -> (rule5 % int2)) triple6) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is young.
True
6
proof
[(((((((triple6) -> rule5) triple6) -> rule6) triple5) -> rule3))]
("Dave" "is" "young" "+")
((((((triple6) -> (rule5 % int3)) triple6) -> (rule6 % int2)) triple5) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is not young.
False
6
inv-proof
[(((((((triple6) -> rule5) triple6) -> rule6) triple5) -> rule3))]
("Dave" "is" "young" "-")
((((((triple6) -> (rule5 % int3)) triple6) -> (rule6 % int2)) triple5) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Fiona is not nice.
Unknown
inv-rconc
[@2: Fiona is nice.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Fiona" "is" "nice" "-")
Fiona is green.
Unknown
rconc
[@2: Fiona is green.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Fiona" "is" "green" "+")
Bob is not young.
Unknown
inv-rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "young" "-")
Fiona is smart.
Unknown
rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "smart" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
@0: Bob is cold.[(triple2)] Bob is green.[(triple3)] Bob is nice.[(triple4)] Bob is not big.[(triple1)] Dave is big.[(triple5)] Dave is smart.[(triple6)] Fiona is not cold.[(triple7)] @1: Dave is green.[(((triple6) -> rule5))] @2: Dave is nice.[(((((triple6) -> rule5) triple6) -> rule6))] @3: Dave is young.[(((((((triple6) -> rule5) triple6) -> rule6) triple5) -> rule3))] @4: Dave is not cold.[(((((((((triple6) -> rule5) triple6) -> rule6) triple5) -> rule3) ((triple6) -> rule5)) -> rule4))]
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Bob is not big.
("Bob" "is" "big" "-")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple5
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Fiona is not cold.
("Fiona" "is" "cold" "-")
triple7
Dave is green.
("Dave" "is" "green" "+")
((triple6) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((((triple6) -> (rule5 % int2)) triple6) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
((((((triple6) -> (rule5 % int3)) triple6) -> (rule6 % int2)) triple5) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is not cold.
("Dave" "is" "cold" "-")
((((((((triple6) -> (rule5 % int4)) triple6) -> (rule6 % int3)) triple5) -> (rule3 % int2)) ((triple6) -> (rule5 % int4))) -> (rule4 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4