Anne is smart. Bob is rough. Charlie is green. Fiona is quiet. Round, rough people are young. If Fiona is green and Fiona is young then Fiona is rough. All white, smart people are rough. Young people are round. If someone is round and rough then they are green. Young people are green. All green people are young. Smart, green people are young.
Anne is smart.
("Anne" "is" "smart" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Round, rough people are young.
((("someone" "is" "round" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
If Fiona is green and Fiona is young then Fiona is rough.
((("Fiona" "is" "green" "+") ("Fiona" "is" "young" "+")) -> ("Fiona" "is" "rough" "+"))
All white, smart people are rough.
((("someone" "is" "white" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
Young people are round.
((("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
If someone is round and rough then they are green.
((("someone" "is" "round" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
Young people are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
All green people are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
Smart, green people are young.
((("someone" "is" "smart" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
Fiona is quiet.
True
1
proof
[(triple4)]
("Fiona" "is" "quiet" "+")
triple4
Anne is not smart.
False
1
inv-proof
[(triple1)]
("Anne" "is" "smart" "-")
triple1
Charlie is young.
True
2
proof
[(((triple3) -> rule7))]
("Charlie" "is" "young" "+")
((triple3) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not young.
False
2
inv-proof
[(((triple3) -> rule7))]
("Charlie" "is" "young" "-")
((triple3) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Anne is not round.
Unknown
inv-rconc
[@5: Anne is round.[CWA. Example of deepest failure = (rule4 <- rule7 <- rule6 <- rule8 <- rule5 <- FAIL)]]
("Anne" "is" "round" "-")
Fiona is rough.
Unknown
rconc
[@5: Fiona is rough.[CWA. Example of deepest failure = (rule2 <- rule6 <- rule7 <- rule5 <- rule3 <- FAIL)]]
("Fiona" "is" "rough" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
@0: Anne is smart.[(triple1)] Bob is rough.[(triple2)] Charlie is green.[(triple3)] Fiona is quiet.[(triple4)] @1: Charlie is young.[(((triple3) -> rule7))] @2: Charlie is round.[(((((triple3) -> rule7)) -> rule4))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
((triple3) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((((triple3) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2