Charlie is green. Charlie is nice. Charlie is quiet. Dave is nice. Dave is young. Fiona is green. Fiona is nice. Green things are young. If something is quiet and green then it is big. If Dave is nice and Dave is green then Dave is young. All quiet things are big. If Fiona is young and Fiona is big then Fiona is cold. All green, quiet things are cold. Young things are green. If something is quiet and big then it is kind.
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Green things are young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If something is quiet and green then it is big.
((("something" "is" "quiet" "+") ("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
If Dave is nice and Dave is green then Dave is young.
((("Dave" "is" "nice" "+") ("Dave" "is" "green" "+")) -> ("Dave" "is" "young" "+"))
All quiet things are big.
((("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
If Fiona is young and Fiona is big then Fiona is cold.
((("Fiona" "is" "young" "+") ("Fiona" "is" "big" "+")) -> ("Fiona" "is" "cold" "+"))
All green, quiet things are cold.
((("something" "is" "green" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
Young things are green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
If something is quiet and big then it is kind.
((("something" "is" "quiet" "+") ("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
Dave is nice.
True
1
proof
[(triple4)]
("Dave" "is" "nice" "+")
triple4
Dave is not young.
False
1
inv-proof
[(triple5)]
("Dave" "is" "young" "-")
triple5
Charlie is young.
True
2
proof
[(((triple1) -> rule1))]
("Charlie" "is" "young" "+")
((triple1) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not cold.
False
3
inv-proof
[(((triple1 triple3) -> rule6))]
("Charlie" "is" "cold" "-")
((triple1 triple3) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is kind.
True
4
proof
[(((triple3 ((triple3) -> rule4)) -> rule8) OR ((triple3 ((triple3 triple1) -> rule2)) -> rule8))]
("Charlie" "is" "kind" "+")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule8 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((triple3 ((triple3 triple1) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not kind.
False
4
inv-proof
[(((triple3 ((triple3) -> rule4)) -> rule8) OR ((triple3 ((triple3 triple1) -> rule2)) -> rule8))]
("Charlie" "is" "kind" "-")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule8 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((triple3 ((triple3 triple1) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "big" "-")
Dave is kind.
Unknown
rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "kind" "+")
Fiona is not cold.
Unknown
inv-rconc
[@2: Fiona is cold.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Fiona" "is" "cold" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
@0: Charlie is green.[(triple1)] Charlie is nice.[(triple2)] Charlie is quiet.[(triple3)] Dave is nice.[(triple4)] Dave is young.[(triple5)] Fiona is green.[(triple6)] Fiona is nice.[(triple7)] @1: Charlie is big.[(((triple3) -> rule4) OR ((triple3 triple1) -> rule2))] Charlie is cold.[(((triple1 triple3) -> rule6))] Charlie is young.[(((triple1) -> rule1))] Dave is green.[(((triple5) -> rule7))] Fiona is young.[(((triple6) -> rule1))] @2: Charlie is kind.[(((triple3 ((triple3) -> rule4)) -> rule8) OR ((triple3 ((triple3 triple1) -> rule2)) -> rule8))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Dave is young.
("Dave" "is" "young" "+")
triple5
Fiona is green.
("Fiona" "is" "green" "+")
triple6
Fiona is nice.
("Fiona" "is" "nice" "+")
triple7
Charlie is big.
("Charlie" "is" "big" "+")
((triple3) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple3 triple1) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple1 triple3) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple1) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple5) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple6) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule8 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((triple3 ((triple3 triple1) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2