Dave is round. Erin is kind. Fiona is blue. All round people are kind. If someone is kind and blue then they are quiet. All kind people are big. All big people are not young. If someone is young and not quiet then they are not cold. If someone is big and not young then they are cold.
Dave is round.
("Dave" "is" "round" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
All round people are kind.
((("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
If someone is kind and blue then they are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
All kind people are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
All big people are not young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "-"))
If someone is young and not quiet then they are not cold.
((("someone" "is" "young" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "cold" "-"))
If someone is big and not young then they are cold.
((("someone" "is" "big" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "cold" "+"))
Dave is round.
True
1
proof
[(triple1)]
("Dave" "is" "round" "+")
triple1
Dave is not round.
False
1
inv-proof
[(triple1)]
("Dave" "is" "round" "-")
triple1
Erin is big.
True
2
proof
[(((triple2) -> rule3))]
("Erin" "is" "big" "+")
((triple2) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not big.
False
2
inv-proof
[(((triple2) -> rule3))]
("Erin" "is" "big" "-")
((triple2) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not quiet.
Unknown
inv-rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "quiet" "-")
Fiona is big.
Unknown
rconc
[@2: Fiona is big.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Fiona" "is" "big" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
@0: Dave is round.[(triple1)] Erin is kind.[(triple2)] Fiona is blue.[(triple3)] @1: Dave is kind.[(((triple1) -> rule1))] Erin is big.[(((triple2) -> rule3))] @2: Dave is big.[(((((triple1) -> rule1)) -> rule3))] Erin is not young.[(((((triple2) -> rule3)) -> rule4))] @3: Dave is not young.[(((((((triple1) -> rule1)) -> rule3)) -> rule4))] Erin is cold.[(((((triple2) -> rule3) ((((triple2) -> rule3)) -> rule4)) -> rule6))] @4: Dave is cold.[(((((((triple1) -> rule1)) -> rule3) ((((((triple1) -> rule1)) -> rule3)) -> rule4)) -> rule6))]
Dave is round.
("Dave" "is" "round" "+")
triple1
Erin is kind.
("Erin" "is" "kind" "+")
triple2
Fiona is blue.
("Fiona" "is" "blue" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
((triple1) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple2) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Erin is not young.
("Erin" "is" "young" "-")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Dave is not young.
("Dave" "is" "young" "-")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is not young.
("Dave" "is" "young" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
((((triple2) -> (rule3 % int3)) ((((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is not young.
("Erin" "is" "young" "-")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
((((((triple1) -> (rule1 % int4))) -> (rule3 % int3)) ((((((triple1) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not young.
("Dave" "is" "young" "-")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4